[STATEMENT]
lemma sym_preproc_addnew_pmdl:
  "pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) = pmdl (set gs \<union> set fs)"
    (is "pmdl (set gs \<union> ?l) = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) = pmdl (set gs \<union> set fs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
have "set gs \<subseteq> set gs \<union> set fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set gs \<subseteq> set gs \<union> set fs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set gs \<subseteq> set gs \<union> set fs

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set gs \<subseteq> set gs \<union> set fs

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
have "... \<subseteq> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set gs \<union> set fs \<subseteq> pmdl (set gs \<union> set fs)
[PROOF STEP]
by (fact pmdl.span_superset)
[PROOF STATE]
proof (state)
this:
set gs \<union> set fs \<subseteq> pmdl (set gs \<union> set fs)

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
set gs \<subseteq> pmdl (set gs \<union> set fs)
[PROOF STEP]
have "set gs \<subseteq> ?r"
[PROOF STATE]
proof (prove)
using this:
set gs \<subseteq> pmdl (set gs \<union> set fs)

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

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set gs \<subseteq> pmdl (set gs \<union> set fs)

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
have "?l \<subseteq> ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (snd (sym_preproc_addnew gs vs fs v)) \<subseteq> pmdl (set gs \<union> set fs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (snd (sym_preproc_addnew gs vs fs v)) \<Longrightarrow> x \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (snd (sym_preproc_addnew gs vs fs v)) \<Longrightarrow> x \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
assume "p \<in> ?l"
[PROOF STATE]
proof (state)
this:
p \<in> set (snd (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. \<And>x. x \<in> set (snd (sym_preproc_addnew gs vs fs v)) \<Longrightarrow> x \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
thus "p \<in> ?r"
[PROOF STATE]
proof (prove)
using this:
p \<in> set (snd (sym_preproc_addnew gs vs fs v))

goal (1 subgoal):
 1. p \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
proof (rule in_snd_sym_preproc_addnewE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p \<in> set fs \<Longrightarrow> p \<in> pmdl (set gs \<union> set fs)
 2. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> p \<in> pmdl (set gs \<union> set fs)
[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> p \<in> pmdl (set gs \<union> set fs)
 2. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> p \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
hence "p \<in> set gs \<union> set fs"
[PROOF STATE]
proof (prove)
using this:
p \<in> set fs

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

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

goal (1 subgoal):
 1. p \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
by (rule pmdl.span_base)
[PROOF STATE]
proof (state)
this:
p \<in> pmdl (set gs \<union> set fs)

goal (1 subgoal):
 1. \<And>g s. \<lbrakk>g \<in> set gs; p = monom_mult (1::'b) s g\<rbrakk> \<Longrightarrow> p \<in> pmdl (set gs \<union> set fs)
[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> p \<in> pmdl (set gs \<union> set fs)
[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> p \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
assume "g \<in> set gs" and p: "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> p \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
from this(1) \<open>set gs \<subseteq> ?r\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> set gs
set gs \<subseteq> pmdl (set gs \<union> set fs)
[PROOF STEP]
have "g \<in> ?r"
[PROOF STATE]
proof (prove)
using this:
g \<in> set gs
set gs \<subseteq> pmdl (set gs \<union> set fs)

goal (1 subgoal):
 1. g \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
g \<in> pmdl (set gs \<union> set fs)

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

goal (1 subgoal):
 1. p \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
unfolding p
[PROOF STATE]
proof (prove)
using this:
g \<in> pmdl (set gs \<union> set fs)

goal (1 subgoal):
 1. monom_mult (1::'b) s g \<in> pmdl (set gs \<union> set fs)
[PROOF STEP]
by (rule pmdl_closed_monom_mult)
[PROOF STATE]
proof (state)
this:
p \<in> pmdl (set gs \<union> set fs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<in> pmdl (set gs \<union> set fs)

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

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set gs \<subseteq> pmdl (set gs \<union> set fs)
set (snd (sym_preproc_addnew gs vs fs v)) \<subseteq> pmdl (set gs \<union> set fs)
[PROOF STEP]
have "set gs \<union> ?l \<subseteq> ?r"
[PROOF STATE]
proof (prove)
using this:
set gs \<subseteq> pmdl (set gs \<union> set fs)
set (snd (sym_preproc_addnew gs vs fs v)) \<subseteq> pmdl (set gs \<union> set fs)

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

goal (2 subgoals):
 1. pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))) \<subseteq> pmdl (set gs \<union> set fs)
 2. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
thus "pmdl (set gs \<union> ?l) \<subseteq> ?r"
[PROOF STATE]
proof (prove)
using this:
set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)) \<subseteq> pmdl (set gs \<union> set fs)

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

goal (1 subgoal):
 1. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (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 "set gs \<union> set fs \<subseteq> set gs \<union> ?l"
[PROOF STATE]
proof (prove)
using this:
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))

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

goal (1 subgoal):
 1. pmdl (set gs \<union> set fs) \<subseteq> pmdl (set gs \<union> set (snd (sym_preproc_addnew gs vs fs v)))
[PROOF STEP]
thus "?r \<subseteq> pmdl (set gs \<union> ?l)"
[PROOF STATE]
proof (prove)
using this:
set gs \<union> set fs \<subseteq> set gs \<union> set (snd (sym_preproc_addnew gs vs fs v))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Keys_snd_sym_preproc_addnew:
  "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::('t \<Rightarrow>\<^sub>0 'b::semiring_1_no_zero_divisors) list) 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]
proof (induct gs arbitrary: vs fs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs fs. Keys (set (snd (sym_preproc_addnew [] vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew [] vs fs v)))
 2. \<And>a gs vs fs. (\<And>vs fs. 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)))) \<Longrightarrow> Keys (set (snd (sym_preproc_addnew (a # gs) vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (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. Keys (set (snd (sym_preproc_addnew [] vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew [] vs fs v)))
 2. \<And>a gs vs fs. (\<And>vs fs. 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)))) \<Longrightarrow> Keys (set (snd (sym_preproc_addnew (a # gs) vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew (a # gs) vs fs v)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew [] vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew [] vs fs v)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Keys (set (snd (sym_preproc_addnew [] vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew [] vs fs v)))

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

goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. 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)))) \<Longrightarrow> Keys (set (snd (sym_preproc_addnew (a # gs) vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew (a # gs) vs fs v)))
[PROOF STEP]
from Cons
[PROOF STATE]
proof (chain)
picking this:
Keys (set (snd (sym_preproc_addnew gs ?vs95 ?fs95 v))) \<union> insert v (set ?vs95) = Keys (set ?fs95) \<union> insert v (set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)))
[PROOF STEP]
have eq: "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set ts') =
                      insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))"
    for ts' fs'
[PROOF STATE]
proof (prove)
using this:
Keys (set (snd (sym_preproc_addnew gs ?vs95 ?fs95 v))) \<union> insert v (set ?vs95) = Keys (set ?fs95) \<union> insert v (set (fst (sym_preproc_addnew gs ?vs95 ?fs95 v)))

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

goal (1 subgoal):
 1. \<And>a gs vs fs. (\<And>vs fs. 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)))) \<Longrightarrow> Keys (set (snd (sym_preproc_addnew (a # gs) vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew (a # gs) vs fs v)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Keys (set (snd (sym_preproc_addnew (g # gs) vs fs v))) \<union> insert v (set vs) = Keys (set fs) \<union> insert v (set (fst (sym_preproc_addnew (g # gs) vs fs v)))
[PROOF STEP]
proof (simp add: Let_def eq, rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
assume "lt g adds\<^sub>t v"
[PROOF STATE]
proof (state)
this:
lt g adds\<^sub>t v

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
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 (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
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 (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
define fs' where "fs' = insert_list f fs"
[PROOF STATE]
proof (state)
this:
fs' = insert_list f fs

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
have "keys (tail f) = keys f - {v}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. keys (tail f) = keys f - {v}
[PROOF STEP]
proof (cases "g = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g = 0 \<Longrightarrow> keys (tail f) = keys f - {v}
 2. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
g = 0

goal (2 subgoals):
 1. g = 0 \<Longrightarrow> keys (tail f) = keys f - {v}
 2. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
hence "f = 0"
[PROOF STATE]
proof (prove)
using this:
g = 0

goal (1 subgoal):
 1. f = 0
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
f = 0

goal (2 subgoals):
 1. g = 0 \<Longrightarrow> keys (tail f) = keys f - {v}
 2. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
f = 0

goal (1 subgoal):
 1. keys (tail f) = keys f - {v}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
keys (tail f) = keys f - {v}

goal (1 subgoal):
 1. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
g \<noteq> 0

goal (1 subgoal):
 1. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
hence "lt f = ?t \<oplus> lt g"
[PROOF STATE]
proof (prove)
using this:
g \<noteq> 0

goal (1 subgoal):
 1. lt f = (pp_of_term v - lp g) \<oplus> lt g
[PROOF STEP]
by (simp add: f_def lt_monom_mult)
[PROOF STATE]
proof (state)
this:
lt f = (pp_of_term v - lp g) \<oplus> lt g

goal (1 subgoal):
 1. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lt f = (pp_of_term v - lp g) \<oplus> lt g

goal (1 subgoal):
 1. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {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. g \<noteq> 0 \<Longrightarrow> keys (tail f) = keys f - {v}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lt f = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lt f = v

goal (1 subgoal):
 1. keys (tail f) = keys f - {v}
[PROOF STEP]
by (simp add: keys_tail)
[PROOF STATE]
proof (state)
this:
keys (tail f) = keys f - {v}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
keys (tail f) = keys f - {v}

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
hence ts': "set ts' = set vs \<union> (keys f - {v})"
[PROOF STATE]
proof (prove)
using this:
keys (tail f) = keys f - {v}

goal (1 subgoal):
 1. set ts' = set vs \<union> (keys f - {v})
[PROOF STEP]
by (simp add: ts'_def set_merge_wrt set_keys_to_list)
[PROOF STATE]
proof (state)
this:
set ts' = set vs \<union> (keys f - {v})

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
have fs': "set fs' = insert f (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set fs' = insert f (set fs)
[PROOF STEP]
by (simp add: fs'_def set_insert_list)
[PROOF STATE]
proof (state)
this:
set fs' = insert f (set fs)

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
hence "f \<in> set fs'"
[PROOF STATE]
proof (prove)
using this:
set fs' = insert f (set fs)

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

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
from this 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 (sym_preproc_addnew gs ts' fs' v))"
[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 ts' fs' v))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f \<in> set (snd (sym_preproc_addnew gs ts' fs' v))

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
hence "keys f \<subseteq> Keys (set (snd (sym_preproc_addnew gs ts' fs' v)))"
[PROOF STATE]
proof (prove)
using this:
f \<in> set (snd (sym_preproc_addnew gs ts' fs' v))

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

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
hence "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set vs) =
          insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set ts')"
[PROOF STATE]
proof (prove)
using this:
keys f \<subseteq> Keys (set (snd (sym_preproc_addnew gs ts' fs' v)))

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

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
also
[PROOF STATE]
proof (state)
this:
insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set vs) = insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set ts')

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
have "... = insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set ts') = insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
by (fact eq)
[PROOF STATE]
proof (state)
this:
insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set ts') = insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
also
[PROOF STATE]
proof (state)
this:
insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set ts') = insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
have "... = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
assume "u \<noteq> v" and "u \<in> keys f"
[PROOF STATE]
proof (state)
this:
u \<noteq> v
u \<in> keys f

goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
hence "u \<in> set ts'"
[PROOF STATE]
proof (prove)
using this:
u \<noteq> v
u \<in> keys f

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

goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
from this fst_sym_preproc_addnew_superset
[PROOF STATE]
proof (chain)
picking this:
u \<in> set ts'
set ?vs \<subseteq> set (fst (sym_preproc_addnew ?gs ?vs ?fs ?v))
[PROOF STEP]
have "u \<in> set (fst (sym_preproc_addnew gs ts' fs' v))"
[PROOF STATE]
proof (prove)
using this:
u \<in> set ts'
set ?vs \<subseteq> set (fst (sym_preproc_addnew ?gs ?vs ?fs ?v))

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

goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u97 \<noteq> v; ?u97 \<in> keys f\<rbrakk> \<Longrightarrow> ?u97 \<in> set (fst (sym_preproc_addnew gs ts' fs' v))

goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u97 \<noteq> v; ?u97 \<in> keys f\<rbrakk> \<Longrightarrow> ?u97 \<in> set (fst (sym_preproc_addnew gs ts' fs' v))

goal (1 subgoal):
 1. insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
by (auto simp add: fs' Keys_insert)
[PROOF STATE]
proof (state)
this:
insert v (Keys (set fs') \<union> set (fst (sym_preproc_addnew gs ts' fs' v))) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))

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

goal (1 subgoal):
 1. lt g adds\<^sub>t v \<Longrightarrow> insert v (Keys (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))) \<union> set vs) = insert v (Keys (set fs) \<union> 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]
finally
[PROOF STATE]
proof (chain)
picking this:
insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set vs) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))
[PROOF STEP]
show "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set vs) =
                  insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))"
[PROOF STATE]
proof (prove)
using this:
insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) \<union> set vs) = insert v (Keys (set fs) \<union> set (fst (sym_preproc_addnew gs ts' fs' v)))

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_preproc_addnew_complete:
  assumes "g \<in> set gs" and "lt g adds\<^sub>t v"
  shows "monom_mult 1 (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs vs fs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs vs fs v))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
g \<in> set gs

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

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

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

goal (1 subgoal):
 1. \<And>a gs vs fs. \<lbrakk>\<And>vs fs. g \<in> set gs \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs vs fs v)); g \<in> set (a # gs)\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> 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. \<lbrakk>\<And>vs fs. g \<in> set gs \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs vs fs v)); g \<in> set (a # gs)\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
case (Cons h gs)
[PROOF STATE]
proof (state)
this:
g \<in> set gs \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs ?vs95 ?fs95 v))
g \<in> set (h # gs)

goal (1 subgoal):
 1. \<And>a gs vs fs. \<lbrakk>\<And>vs fs. g \<in> set gs \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs vs fs v)); g \<in> set (a # gs)\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
let ?t = "pp_of_term v - lp g"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a gs vs fs. \<lbrakk>\<And>vs fs. g \<in> set gs \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew gs vs fs v)); g \<in> set (a # gs)\<rbrakk> \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (a # gs) vs fs v))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
proof (cases "h = g")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. h = g \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
 2. h \<noteq> g \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
h = g

goal (2 subgoals):
 1. h = g \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
 2. h \<noteq> g \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
proof (simp add: True assms(2) Let_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<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))
[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 (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<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))
[PROOF STEP]
define ts' where "ts' = merge_wrt (\<succ>\<^sub>t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
[PROOF STATE]
proof (state)
this:
ts' = 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. monom_mult (1::'b) (pp_of_term v - lp g) g \<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))
[PROOF STEP]
have "f \<in> set (insert_list f fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> set (insert_list f fs)
[PROOF STEP]
by (simp add: set_insert_list)
[PROOF STATE]
proof (state)
this:
f \<in> set (insert_list f fs)

goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<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))
[PROOF STEP]
with snd_sym_preproc_addnew_superset
[PROOF STATE]
proof (chain)
picking this:
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))
f \<in> set (insert_list f fs)
[PROOF STEP]
show "f \<in> set (snd (sym_preproc_addnew gs ts' (insert_list f fs) v))"
[PROOF STATE]
proof (prove)
using this:
set ?fs \<subseteq> set (snd (sym_preproc_addnew ?gs ?vs ?fs ?v))
f \<in> set (insert_list f fs)

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

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

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

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

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

goal (1 subgoal):
 1. h \<noteq> g \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
hence *: "monom_mult 1 ?t g \<in> set (snd (sym_preproc_addnew gs ts' fs' v))" for ts' fs'
[PROOF STATE]
proof (prove)
using this:
g \<in> set gs

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

goal (1 subgoal):
 1. h \<noteq> g \<Longrightarrow> monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))
[PROOF STEP]
by (simp add: Let_def *)
[PROOF STATE]
proof (state)
this:
monom_mult (1::'b) (pp_of_term v - lp g) g \<in> set (snd (sym_preproc_addnew (h # gs) vs fs v))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_preproc_aux_Nil: "sym_preproc_aux gs ks ([], fs) = (ks, fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_preproc_aux gs ks ([], fs) = (ks, fs)
[PROOF STEP]
by simp


[STATEMENT]
lemma sym_preproc_aux_sorted:
  assumes "sorted_wrt (\<succ>\<^sub>t) (v # vs)"
  shows "sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sorted_wrt (\<succ>\<^sub>t) (v # vs)
[PROOF STEP]
have *: "u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v" for u
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<succ>\<^sub>t) (v # vs)

goal (1 subgoal):
 1. u \<in> set vs \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?u100 \<in> set vs \<Longrightarrow> ?u100 \<prec>\<^sub>t v

goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
have "ord_term_lin.max_list (v # vs) = ord_term_lin.Max (set (v # vs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_term_lin.max_list (v # vs) = ord_term_lin.Max (set (v # vs))
[PROOF STEP]
by (simp add: ord_term_lin.max_list_Max del: ord_term_lin.max_list.simps)
[PROOF STATE]
proof (state)
this:
ord_term_lin.max_list (v # vs) = ord_term_lin.Max (set (v # vs))

goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ord_term_lin.max_list (v # vs) = ord_term_lin.Max (set (v # vs))

goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
have "... = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_term_lin.Max (set (v # vs)) = v
[PROOF STEP]
proof (rule ord_term_lin.Max_eqI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite (set (v # vs))
 2. \<And>y. y \<in> set (v # vs) \<Longrightarrow> y \<preceq>\<^sub>t v
 3. v \<in> set (v # vs)
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite (set (v # vs))
 2. \<And>y. y \<in> set (v # vs) \<Longrightarrow> y \<preceq>\<^sub>t v
 3. v \<in> set (v # vs)
[PROOF STEP]
assume "s \<in> set (v # vs)"
[PROOF STATE]
proof (state)
this:
s \<in> set (v # vs)

goal (3 subgoals):
 1. finite (set (v # vs))
 2. \<And>y. y \<in> set (v # vs) \<Longrightarrow> y \<preceq>\<^sub>t v
 3. v \<in> set (v # vs)
[PROOF STEP]
hence "s = v \<or> s \<in> set vs"
[PROOF STATE]
proof (prove)
using this:
s \<in> set (v # vs)

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

goal (3 subgoals):
 1. finite (set (v # vs))
 2. \<And>y. y \<in> set (v # vs) \<Longrightarrow> y \<preceq>\<^sub>t v
 3. v \<in> set (v # vs)
[PROOF STEP]
thus "s \<preceq>\<^sub>t v"
[PROOF STATE]
proof (prove)
using this:
s = v \<or> s \<in> set vs

goal (1 subgoal):
 1. s \<preceq>\<^sub>t v
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. s = v \<Longrightarrow> s \<preceq>\<^sub>t v
 2. s \<in> set vs \<Longrightarrow> s \<preceq>\<^sub>t v
[PROOF STEP]
assume "s = v"
[PROOF STATE]
proof (state)
this:
s = v

goal (2 subgoals):
 1. s = v \<Longrightarrow> s \<preceq>\<^sub>t v
 2. s \<in> set vs \<Longrightarrow> s \<preceq>\<^sub>t v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s = v

goal (1 subgoal):
 1. s \<preceq>\<^sub>t v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<preceq>\<^sub>t v

goal (1 subgoal):
 1. s \<in> set vs \<Longrightarrow> s \<preceq>\<^sub>t v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> set vs \<Longrightarrow> s \<preceq>\<^sub>t v
[PROOF STEP]
assume "s \<in> set vs"
[PROOF STATE]
proof (state)
this:
s \<in> set vs

goal (1 subgoal):
 1. s \<in> set vs \<Longrightarrow> s \<preceq>\<^sub>t v
[PROOF STEP]
hence "s \<prec>\<^sub>t v"
[PROOF STATE]
proof (prove)
using this:
s \<in> set vs

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

goal (1 subgoal):
 1. s \<in> set vs \<Longrightarrow> s \<preceq>\<^sub>t v
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<prec>\<^sub>t v

goal (1 subgoal):
 1. s \<preceq>\<^sub>t v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s \<preceq>\<^sub>t v

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

goal (2 subgoals):
 1. finite (set (v # vs))
 2. v \<in> set (v # vs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (set (v # vs))
 2. v \<in> set (v # vs)
[PROOF STEP]
show "v \<in> set (v # vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> set (v # vs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> set (v # vs)

goal (1 subgoal):
 1. finite (set (v # vs))
[PROOF STEP]
qed rule
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (v # vs)) = v

goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ord_term_lin.max_list (v # vs) = v
[PROOF STEP]
have eq1: "ord_term_lin.max_list (v # vs) = v"
[PROOF STATE]
proof (prove)
using this:
ord_term_lin.max_list (v # vs) = v

goal (1 subgoal):
 1. ord_term_lin.max_list (v # vs) = v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ord_term_lin.max_list (v # vs) = v

goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
have eq2: "removeAll v (v # vs) = vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. removeAll v (v # vs) = vs
[PROOF STEP]
proof (simp, rule removeAll_id, rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> set vs \<Longrightarrow> False
[PROOF STEP]
assume "v \<in> set vs"
[PROOF STATE]
proof (state)
this:
v \<in> set vs

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

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

goal (1 subgoal):
 1. v \<in> set vs \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
v \<prec>\<^sub>t v

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
removeAll v (v # vs) = vs

goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)
[PROOF STEP]
by (simp only: sym_preproc_aux.simps eq1 eq2 Let_def, simp)
[PROOF STATE]
proof (state)
this:
sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_preproc_aux_induct [consumes 0, case_names base rec]:
  assumes base: "\<And>ks fs. P ks [] fs (ks, fs)"
    and rec: "\<And>ks vs fs v vs'. vs \<noteq> [] \<Longrightarrow> v = ord_term_lin.Max (set vs) \<Longrightarrow> vs' = removeAll v vs \<Longrightarrow>
                P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v))
                    (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)) \<Longrightarrow>
                P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))"
  shows "P ks vs fs (sym_preproc_aux gs ks (vs, fs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
from ex_dgrad
[PROOF STATE]
proof (chain)
picking this:
\<exists>d. dickson_grading d
[PROOF STEP]
obtain d::"'a \<Rightarrow> nat" where dg: "dickson_grading d"
[PROOF STATE]
proof (prove)
using this:
\<exists>d. dickson_grading d

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

goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
let ?R = "(sym_preproc_aux_term d)::((('t \<Rightarrow>\<^sub>0 'b) list \<times> 't list \<times> 't list \<times> ('t \<Rightarrow>\<^sub>0 'b) list) \<times>
                                        ('t \<Rightarrow>\<^sub>0 'b) list \<times> 't list \<times> 't list \<times> ('t \<Rightarrow>\<^sub>0 'b) list) set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
define args where "args = (gs, ks, vs, fs)"
[PROOF STATE]
proof (state)
this:
args = (gs, ks, vs, fs)

goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
from dg
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "wf ?R"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. wf (sym_preproc_aux_term d)
[PROOF STEP]
by (rule sym_preproc_aux_term_wf)
[PROOF STATE]
proof (state)
this:
wf (sym_preproc_aux_term d)

goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
hence "fst args = gs \<Longrightarrow> P (fst (snd args)) (fst (snd (snd args))) (snd (snd (snd args)))
                              (sym_preproc_aux gs (fst (snd args)) (snd (snd args)))"
[PROOF STATE]
proof (prove)
using this:
wf (sym_preproc_aux_term d)

goal (1 subgoal):
 1. fst args = gs \<Longrightarrow> P (fst (snd args)) (fst (snd (snd args))) (snd (snd (snd args))) (sym_preproc_aux gs (fst (snd args)) (snd (snd args)))
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
assume IH': "\<And>y. (y, x) \<in> sym_preproc_aux_term d \<Longrightarrow> fst y = gs \<Longrightarrow>
                    P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y)))
                      (sym_preproc_aux gs (fst (snd y)) (snd (snd y)))"
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?y100, x) \<in> sym_preproc_aux_term d; fst ?y100 = gs\<rbrakk> \<Longrightarrow> P (fst (snd ?y100)) (fst (snd (snd ?y100))) (snd (snd (snd ?y100))) (sym_preproc_aux gs (fst (snd ?y100)) (snd (snd ?y100)))

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
assume "fst x = gs"
[PROOF STATE]
proof (state)
this:
fst x = gs

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst x = gs
[PROOF STEP]
obtain x0 where x: "x = (gs, x0)"
[PROOF STATE]
proof (prove)
using this:
fst x = gs

goal (1 subgoal):
 1. (\<And>x0. x = (gs, x0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson eq_fst_iff)
[PROOF STATE]
proof (state)
this:
x = (gs, x0)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
obtain ks x1 where x0: "x0 = (ks, x1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ks x1. x0 = (ks, x1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson case_prodE case_prodI2)
[PROOF STATE]
proof (state)
this:
x0 = (ks, x1)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
obtain vs fs where x1: "x1 = (vs, fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vs fs. x1 = (vs, fs) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson case_prodE case_prodI2)
[PROOF STATE]
proof (state)
this:
x1 = (vs, fs)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
from IH'
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?y100, x) \<in> sym_preproc_aux_term d; fst ?y100 = gs\<rbrakk> \<Longrightarrow> P (fst (snd ?y100)) (fst (snd (snd ?y100))) (snd (snd (snd ?y100))) (sym_preproc_aux gs (fst (snd ?y100)) (snd (snd ?y100)))
[PROOF STEP]
have IH: "\<And>ks' n. ((gs, ks', n), (gs, ks, vs, fs)) \<in> sym_preproc_aux_term d \<Longrightarrow>
                            P ks' (fst n) (snd n) (sym_preproc_aux gs ks' n)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?y100, x) \<in> sym_preproc_aux_term d; fst ?y100 = gs\<rbrakk> \<Longrightarrow> P (fst (snd ?y100)) (fst (snd (snd ?y100))) (snd (snd (snd ?y100))) (sym_preproc_aux gs (fst (snd ?y100)) (snd (snd ?y100)))

goal (1 subgoal):
 1. \<And>ks' n. ((gs, ks', n), gs, ks, vs, fs) \<in> sym_preproc_aux_term d \<Longrightarrow> P ks' (fst n) (snd n) (sym_preproc_aux gs ks' n)
[PROOF STEP]
unfolding x x0 x1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?y100, gs, ks, vs, fs) \<in> sym_preproc_aux_term d; fst ?y100 = gs\<rbrakk> \<Longrightarrow> P (fst (snd ?y100)) (fst (snd (snd ?y100))) (snd (snd (snd ?y100))) (sym_preproc_aux gs (fst (snd ?y100)) (snd (snd ?y100)))

goal (1 subgoal):
 1. \<And>ks' n. ((gs, ks', n), gs, ks, vs, fs) \<in> sym_preproc_aux_term d \<Longrightarrow> P ks' (fst n) (snd n) (sym_preproc_aux gs ks' n)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
((gs, ?ks'100, ?n100), gs, ks, vs, fs) \<in> sym_preproc_aux_term d \<Longrightarrow> P ?ks'100 (fst ?n100) (snd ?n100) (sym_preproc_aux gs ?ks'100 ?n100)

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>(y, x) \<in> sym_preproc_aux_term d; fst y = gs\<rbrakk> \<Longrightarrow> P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y))) (sym_preproc_aux gs (fst (snd y)) (snd (snd y))); fst x = gs\<rbrakk> \<Longrightarrow> P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
show "P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x)))
            (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))
[PROOF STEP]
proof (simp add: x x0 x1 Let_def, intro conjI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vs = [] \<Longrightarrow> P ks [] fs (ks, fs)
 2. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
show "P ks [] fs (ks, fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ks [] fs (ks, fs)
[PROOF STEP]
by (fact base)
[PROOF STATE]
proof (state)
this:
P ks [] fs (ks, fs)

goal (1 subgoal):
 1. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
assume "vs \<noteq> []"
[PROOF STATE]
proof (state)
this:
vs \<noteq> []

goal (1 subgoal):
 1. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
define v where "v = ord_term_lin.max_list vs"
[PROOF STATE]
proof (state)
this:
v = ord_term_lin.max_list vs

goal (1 subgoal):
 1. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
from \<open>vs \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
vs \<noteq> []
[PROOF STEP]
have v_alt: "v = ord_term_lin.Max (set vs)"
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []

goal (1 subgoal):
 1. v = ord_term_lin.Max (set vs)
[PROOF STEP]
unfolding v_def
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []

goal (1 subgoal):
 1. ord_term_lin.max_list vs = ord_term_lin.Max (set vs)
[PROOF STEP]
by (rule ord_term_lin.max_list_Max)
[PROOF STATE]
proof (state)
this:
v = ord_term_lin.Max (set vs)

goal (1 subgoal):
 1. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
define vs' where "vs' = removeAll v vs"
[PROOF STATE]
proof (state)
this:
vs' = removeAll v vs

goal (1 subgoal):
 1. vs \<noteq> [] \<Longrightarrow> P ks vs fs (sym_preproc_aux gs (ks @ [ord_term_lin.max_list vs]) (sym_preproc_addnew gs (removeAll (ord_term_lin.max_list vs) vs) fs (ord_term_lin.max_list vs)))
[PROOF STEP]
show "P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
proof (rule rec, fact \<open>vs \<noteq> []\<close>, fact v_alt, fact vs'_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v)) (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
let ?n = "sym_preproc_addnew gs vs' fs v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v)) (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
obtain vs0 fs0 where eq: "?n = (vs0, fs0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vs0 fs0. sym_preproc_addnew gs vs' fs v = (vs0, fs0) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sym_preproc_addnew gs vs' fs v = (vs0, fs0)

goal (1 subgoal):
 1. P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v)) (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
show "P (ks @ [v]) (fst ?n) (snd ?n) (sym_preproc_aux gs (ks @ [v]) ?n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v)) (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
proof (rule IH,
              simp add: eq sym_preproc_aux_term_def sym_preproc_aux_term1_def sym_preproc_aux_term2_def,
              intro conjI bexI ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t1. t1 \<in> set vs0 \<Longrightarrow> t1 \<prec>\<^sub>t ?t2.103
 2. ?t2.103 \<in> set vs
 3. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>t1. t1 \<in> set vs0 \<Longrightarrow> t1 \<prec>\<^sub>t ?t2.103
 2. ?t2.103 \<in> set vs
 3. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
assume "s \<in> set vs0"
[PROOF STATE]
proof (state)
this:
s \<in> set vs0

goal (3 subgoals):
 1. \<And>t1. t1 \<in> set vs0 \<Longrightarrow> t1 \<prec>\<^sub>t ?t2.103
 2. ?t2.103 \<in> set vs
 3. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
show "s \<prec>\<^sub>t v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<prec>\<^sub>t v
[PROOF STEP]
proof (rule fst_sym_preproc_addnew_less)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. u \<in> set ?vs \<Longrightarrow> u \<prec>\<^sub>t v
 2. s \<in> set (fst (sym_preproc_addnew ?gs ?vs ?fs v))
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. u \<in> set ?vs \<Longrightarrow> u \<prec>\<^sub>t v
 2. s \<in> set (fst (sym_preproc_addnew ?gs ?vs ?fs v))
[PROOF STEP]
assume "u \<in> set vs'"
[PROOF STATE]
proof (state)
this:
u \<in> set vs'

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

goal (1 subgoal):
 1. u \<prec>\<^sub>t v
[PROOF STEP]
unfolding vs'_def v_alt set_removeAll
[PROOF STATE]
proof (prove)
using this:
u \<in> set vs - {ord_term_lin.Max (set vs)}

goal (1 subgoal):
 1. u \<prec>\<^sub>t ord_term_lin.Max (set vs)
[PROOF STEP]
using ord_term_lin.antisym_conv1
[PROOF STATE]
proof (prove)
using this:
u \<in> set vs - {ord_term_lin.Max (set vs)}
\<not> ?x \<prec>\<^sub>t ?y \<Longrightarrow> (?x \<preceq>\<^sub>t ?y) = (?x = ?y)

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

goal (1 subgoal):
 1. s \<in> set (fst (sym_preproc_addnew ?gs vs' ?fs v))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s \<in> set (fst (sym_preproc_addnew ?gs vs' ?fs v))
[PROOF STEP]
from \<open>s \<in> set vs0\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> set vs0
[PROOF STEP]
show "s \<in> set (fst (sym_preproc_addnew gs vs' fs v))"
[PROOF STATE]
proof (prove)
using this:
s \<in> set vs0

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

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

goal (2 subgoals):
 1. v \<in> set vs
 2. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> set vs
 2. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
from \<open>vs \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
vs \<noteq> []
[PROOF STEP]
show "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: v_alt)
[PROOF STATE]
proof (state)
this:
v \<in> set vs

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
from dg
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "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)
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 ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
moreover
[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 ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
have "insert v (set vs') = set vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert v (set vs') = set vs
[PROOF STEP]
by (auto simp add: vs'_def v_alt \<open>vs \<noteq> []\<close>)
[PROOF STATE]
proof (state)
this:
insert v (set vs') = set vs

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking 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')))
insert v (set vs') = set vs
[PROOF STEP]
show "dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))"
[PROOF STATE]
proof (prove)
using 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')))
insert v (set vs') = set vs

goal (1 subgoal):
 1. dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))
[PROOF STEP]
by (simp add: eq)
[PROOF STATE]
proof (state)
this:
dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) \<union> set vs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v)) (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x))) (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fst args = gs \<Longrightarrow> P (fst (snd args)) (fst (snd (snd args))) (snd (snd (snd args))) (sym_preproc_aux gs (fst (snd args)) (snd (snd args)))

goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fst args = gs \<Longrightarrow> P (fst (snd args)) (fst (snd (snd args))) (snd (snd (snd args))) (sym_preproc_aux gs (fst (snd args)) (snd (snd args)))

goal (1 subgoal):
 1. P ks vs fs (sym_preproc_aux gs ks (vs, fs))
[PROOF STEP]
by (simp add: args_def)
[PROOF STATE]
proof (state)
this:
P ks vs fs (sym_preproc_aux gs ks (vs, fs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_sym_preproc_aux_sorted_wrt:
  assumes "sorted_wrt (\<succ>\<^sub>t) ks" and "\<And>k v. k \<in> set ks \<Longrightarrow> v \<in> set vs \<Longrightarrow> v \<prec>\<^sub>t k"
  shows "sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs ks (vs, fs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs ks (vs, fs)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<succ>\<^sub>t) ks
\<lbrakk>?k100 \<in> set ks; ?v100 \<in> set vs\<rbrakk> \<Longrightarrow> ?v100 \<prec>\<^sub>t ?k100

goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (fst (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. \<lbrakk>sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set []\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (ks, fs))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set vs\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
case (base ks fs)
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<succ>\<^sub>t) ks
\<lbrakk>?k100 \<in> set ks; ?v100 \<in> set []\<rbrakk> \<Longrightarrow> ?v100 \<prec>\<^sub>t ?k100

goal (2 subgoals):
 1. \<And>ks fs. \<lbrakk>sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set []\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (ks, fs))
 2. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set vs\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
from base(1)
[PROOF STATE]
proof (chain)
picking this:
sorted_wrt (\<succ>\<^sub>t) ks
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sorted_wrt (\<succ>\<^sub>t) ks

goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (fst (ks, fs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<succ>\<^sub>t) (fst (ks, fs))

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set vs\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set vs\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
case (rec ks vs fs v vs')
[PROOF STATE]
proof (state)
this:
vs \<noteq> []
v = ord_term_lin.Max (set vs)
vs' = removeAll v vs
\<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
sorted_wrt (\<succ>\<^sub>t) ks
\<lbrakk>?k100 \<in> set ks; ?v100 \<in> set vs\<rbrakk> \<Longrightarrow> ?v100 \<prec>\<^sub>t ?k100

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

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

goal (1 subgoal):
 1. \<And>ks vs fs v vs'. \<lbrakk>vs \<noteq> []; v = ord_term_lin.Max (set vs); vs' = removeAll v vs; \<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set vs\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (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 *: "\<And>u. u \<in> set vs' \<Longrightarrow> u \<prec>\<^sub>t v"
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []

goal (1 subgoal):
 1. \<And>u. u \<in> set vs' \<Longrightarrow> u \<prec>\<^sub>t v
[PROOF STEP]
unfolding rec(2, 3) set_removeAll
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []

goal (1 subgoal):
 1. \<And>u. u \<in> set vs - {ord_term_lin.Max (set vs)} \<Longrightarrow> u \<prec>\<^sub>t ord_term_lin.Max (set vs)
[PROOF STEP]
using ord_term_lin.antisym_conv3
[PROOF STATE]
proof (prove)
using this:
vs \<noteq> []
\<not> ?y \<prec>\<^sub>t ?x \<Longrightarrow> (\<not> ?x \<prec>\<^sub>t ?y) = (?x = ?y)

goal (1 subgoal):
 1. \<And>u. u \<in> set vs - {ord_term_lin.Max (set vs)} \<Longrightarrow> u \<prec>\<^sub>t ord_term_lin.Max (set vs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
?u100 \<in> set vs' \<Longrightarrow> ?u100 \<prec>\<^sub>t 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; \<lbrakk>sorted_wrt (\<succ>\<^sub>t) (ks @ [v]); \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))); sorted_wrt (\<succ>\<^sub>t) ks; \<And>k v. \<lbrakk>k \<in> set ks; v \<in> set vs\<rbrakk> \<Longrightarrow> v \<prec>\<^sub>t k\<rbrakk> \<Longrightarrow> sorted_wrt (\<succ>\<^sub>t) (fst (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. sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))
[PROOF STEP]
proof (rule rec(4))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sorted_wrt (\<succ>\<^sub>t) (ks @ [v])
 2. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
show "sorted_wrt (\<succ>\<^sub>t) (ks @ [v])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted_wrt (\<succ>\<^sub>t) (ks @ [v])
[PROOF STEP]
proof (simp add: sorted_wrt_append rec(5), rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set ks \<Longrightarrow> v \<prec>\<^sub>t x
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set ks \<Longrightarrow> v \<prec>\<^sub>t x
[PROOF STEP]
assume "k \<in> set ks"
[PROOF STATE]
proof (state)
this:
k \<in> set ks

goal (1 subgoal):
 1. \<And>x. x \<in> set ks \<Longrightarrow> v \<prec>\<^sub>t x
[PROOF STEP]
from this \<open>v \<in> set vs\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> set ks
v \<in> set vs
[PROOF STEP]
show "v \<prec>\<^sub>t k"
[PROOF STATE]
proof (prove)
using this:
k \<in> set ks
v \<in> set vs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<succ>\<^sub>t) (ks @ [v])

goal (1 subgoal):
 1. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
fix k u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
assume "k \<in> set (ks @ [v])" and "u \<in> set (fst (sym_preproc_addnew gs vs' fs v))"
[PROOF STATE]
proof (state)
this:
k \<in> set (ks @ [v])
u \<in> set (fst (sym_preproc_addnew gs vs' fs v))

goal (1 subgoal):
 1. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
from * this(2)
[PROOF STATE]
proof (chain)
picking this:
?u100 \<in> set vs' \<Longrightarrow> ?u100 \<prec>\<^sub>t v
u \<in> set (fst (sym_preproc_addnew gs vs' fs v))
[PROOF STEP]
have "u \<prec>\<^sub>t v"
[PROOF STATE]
proof (prove)
using this:
?u100 \<in> set vs' \<Longrightarrow> ?u100 \<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 fst_sym_preproc_addnew_less)
[PROOF STATE]
proof (state)
this:
u \<prec>\<^sub>t v

goal (1 subgoal):
 1. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
from \<open>k \<in> set (ks @ [v])\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> set (ks @ [v])
[PROOF STEP]
have "k \<in> set ks \<or> k = v"
[PROOF STATE]
proof (prove)
using this:
k \<in> set (ks @ [v])

goal (1 subgoal):
 1. k \<in> set ks \<or> k = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k \<in> set ks \<or> k = v

goal (1 subgoal):
 1. \<And>k va. \<lbrakk>k \<in> set (ks @ [v]); va \<in> set (fst (sym_preproc_addnew gs vs' fs v))\<rbrakk> \<Longrightarrow> va \<prec>\<^sub>t k
[PROOF STEP]
thus "u \<prec>\<^sub>t k"
[PROOF STATE]
proof (prove)
using this:
k \<in> set ks \<or> k = v

goal (1 subgoal):
 1. u \<prec>\<^sub>t k
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k \<in> set ks \<Longrightarrow> u \<prec>\<^sub>t k
 2. k = v \<Longrightarrow> u \<prec>\<^sub>t k
[PROOF STEP]
assume "k \<in> set ks"
[PROOF STATE]
proof (state)
this:
k \<in> set ks

goal (2 subgoals):
 1. k \<in> set ks \<Longrightarrow> u \<prec>\<^sub>t k
 2. k = v \<Longrightarrow> u \<prec>\<^sub>t k
[PROOF STEP]
from this \<open>v \<in> set vs\<close>
[PROOF STATE]
proof (chain)
picking this:
k \<in> set ks
v \<in> set vs
[PROOF STEP]
have "v \<prec>\<^sub>t k"
[PROOF STATE]
proof (prove)
using this:
k \<in> set ks
v \<in> set vs

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

goal (2 subgoals):
 1. k \<in> set ks \<Longrightarrow> u \<prec>\<^sub>t k
 2. k = v \<Longrightarrow> u \<prec>\<^sub>t k
[PROOF STEP]
with \<open>u \<prec>\<^sub>t v\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<prec>\<^sub>t v
v \<prec>\<^sub>t k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<prec>\<^sub>t v
v \<prec>\<^sub>t k

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

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

goal (1 subgoal):
 1. k = v \<Longrightarrow> u \<prec>\<^sub>t k
[PROOF STEP]
with \<open>u \<prec>\<^sub>t v\<close>
[PROOF STATE]
proof (chain)
picking this:
u \<prec>\<^sub>t v
k = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<prec>\<^sub>t v
k = v

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sorted_wrt (\<succ>\<^sub>t) (fst (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)))

goal:
No subgoals!
[PROOF STEP]
qed