[STATEMENT]
lemma list_order_monotonic:
  assumes "insert_ops A" and "insert_ops B"
    and "set A \<subseteq> set B"
    and "list_order A x y"
  shows "list_order B x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_order B x y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
insert_ops A
insert_ops B
set A \<subseteq> set B
list_order A x y

goal (1 subgoal):
 1. list_order B x y
[PROOF STEP]
proof(induction rule: measure_induct_rule[where f="\<lambda>x. (length x - length A)"])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>ya. \<lbrakk>length ya - length A < length xa - length A; insert_ops A; insert_ops ya; set A \<subseteq> set ya; list_order A x y\<rbrakk> \<Longrightarrow> list_order ya x y; insert_ops A; insert_ops xa; set A \<subseteq> set xa; list_order A x y\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case (less xa)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?y - length A < length xa - length A; insert_ops A; insert_ops ?y; set A \<subseteq> set ?y; list_order A x y\<rbrakk> \<Longrightarrow> list_order ?y x y
insert_ops A
insert_ops xa
set A \<subseteq> set xa
list_order A x y

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>ya. \<lbrakk>length ya - length A < length xa - length A; insert_ops A; insert_ops ya; set A \<subseteq> set ya; list_order A x y\<rbrakk> \<Longrightarrow> list_order ya x y; insert_ops A; insert_ops xa; set A \<subseteq> set xa; list_order A x y\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
have "distinct (map fst A)" and "distinct (map fst xa)" and
    "sorted (map fst A)" and "sorted (map fst xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (distinct (map fst A) &&& distinct (map fst xa)) &&& sorted (map fst A) &&& sorted (map fst xa)
[PROOF STEP]
using less.prems
[PROOF STATE]
proof (prove)
using this:
insert_ops A
insert_ops xa
set A \<subseteq> set xa
list_order A x y

goal (1 subgoal):
 1. (distinct (map fst A) &&& distinct (map fst xa)) &&& sorted (map fst A) &&& sorted (map fst xa)
[PROOF STEP]
by (auto simp add: insert_ops_def spec_ops_def)
[PROOF STATE]
proof (state)
this:
distinct (map fst A)
distinct (map fst xa)
sorted (map fst A)
sorted (map fst xa)

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>ya. \<lbrakk>length ya - length A < length xa - length A; insert_ops A; insert_ops ya; set A \<subseteq> set ya; list_order A x y\<rbrakk> \<Longrightarrow> list_order ya x y; insert_ops A; insert_ops xa; set A \<subseteq> set xa; list_order A x y\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "distinct A" and "distinct xa"
[PROOF STATE]
proof (prove)
using this:
distinct (map fst A)
distinct (map fst xa)
sorted (map fst A)
sorted (map fst xa)

goal (1 subgoal):
 1. distinct A &&& distinct xa
[PROOF STEP]
by (auto simp add: distinct_fst)
[PROOF STATE]
proof (state)
this:
distinct A
distinct xa

goal (1 subgoal):
 1. \<And>xa. \<lbrakk>\<And>ya. \<lbrakk>length ya - length A < length xa - length A; insert_ops A; insert_ops ya; set A \<subseteq> set ya; list_order A x y\<rbrakk> \<Longrightarrow> list_order ya x y; insert_ops A; insert_ops xa; set A \<subseteq> set xa; list_order A x y\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct A
distinct xa
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
distinct A
distinct xa

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
proof(cases "length xa - length A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct A; distinct xa; length xa - length A = 0\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
length xa - length A = 0

goal (2 subgoals):
 1. \<lbrakk>distinct A; distinct xa; length xa - length A = 0\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "set A = set xa"
[PROOF STATE]
proof (prove)
using this:
length xa - length A = 0

goal (1 subgoal):
 1. set A = set xa
[PROOF STEP]
using set_subset_length_eq less.prems(3) \<open>distinct A\<close> \<open>distinct xa\<close> diff_is_0_eq
[PROOF STATE]
proof (prove)
using this:
length xa - length A = 0
\<lbrakk>set ?A \<subseteq> set ?B; length ?B \<le> length ?A; distinct ?A; distinct ?B\<rbrakk> \<Longrightarrow> set ?A = set ?B
set A \<subseteq> set xa
distinct A
distinct xa
(?m - ?n = 0) = (?m \<le> ?n)

goal (1 subgoal):
 1. set A = set xa
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set A = set xa

goal (2 subgoals):
 1. \<lbrakk>distinct A; distinct xa; length xa - length A = 0\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "A = xa"
[PROOF STATE]
proof (prove)
using this:
set A = set xa

goal (1 subgoal):
 1. A = xa
[PROOF STEP]
using \<open>distinct (map fst A)\<close> \<open>distinct (map fst xa)\<close>
        \<open>sorted (map fst A)\<close> \<open>sorted (map fst xa)\<close> map_sorted_distinct_set_unique
[PROOF STATE]
proof (prove)
using this:
set A = set xa
distinct (map fst A)
distinct (map fst xa)
sorted (map fst A)
sorted (map fst xa)
\<lbrakk>inj_on ?f (set ?xs \<union> set ?ys); sorted (map ?f ?xs); distinct (map ?f ?xs); sorted (map ?f ?ys); distinct (map ?f ?ys); set ?xs = set ?ys\<rbrakk> \<Longrightarrow> ?xs = ?ys

goal (1 subgoal):
 1. A = xa
[PROOF STEP]
by (metis distinct_map less.prems(3) subset_Un_eq)
[PROOF STATE]
proof (state)
this:
A = xa

goal (2 subgoals):
 1. \<lbrakk>distinct A; distinct xa; length xa - length A = 0\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = xa
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
A = xa

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
using less.prems(4)
[PROOF STATE]
proof (prove)
using this:
A = xa
list_order A x y

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case (Suc nat)
[PROOF STATE]
proof (state)
this:
length xa - length A = Suc nat

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xa - length A = Suc nat
[PROOF STEP]
obtain e where "e \<in> set xa" and "e \<notin> set A"
[PROOF STATE]
proof (prove)
using this:
length xa - length A = Suc nat

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using length_diff_Suc_exists \<open>distinct A\<close> \<open>distinct xa\<close> less.prems(3)
[PROOF STATE]
proof (prove)
using this:
length xa - length A = Suc nat
\<lbrakk>length ?xs - length ?ys = Suc ?m; set ?ys \<subseteq> set ?xs; distinct ?ys; distinct ?xs\<rbrakk> \<Longrightarrow> \<exists>e. e \<in> set ?xs \<and> e \<notin> set ?ys
distinct A
distinct xa
set A \<subseteq> set xa

goal (1 subgoal):
 1. (\<And>e. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
e \<in> set xa
e \<notin> set A

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence IH: "list_order (remove1 e xa) x y"
[PROOF STATE]
proof (prove)
using this:
e \<in> set xa
e \<notin> set A

goal (1 subgoal):
 1. list_order (remove1 e xa) x y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> list_order (remove1 e xa) x y
[PROOF STEP]
have "length (remove1 e xa) - length A < Suc nat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (remove1 e xa) - length A < Suc nat
[PROOF STEP]
using diff_Suc_1 diff_commute length_remove1 less_Suc_eq Suc \<open>e \<in> set xa\<close>
[PROOF STATE]
proof (prove)
using this:
Suc ?n - 1 = ?n
?i - ?j - ?k = ?i - ?k - ?j
length (remove1 ?x ?xs) = (if ?x \<in> set ?xs then length ?xs - 1 else length ?xs)
(?m < Suc ?n) = (?m < ?n \<or> ?m = ?n)
length xa - length A = Suc nat
e \<in> set xa

goal (1 subgoal):
 1. length (remove1 e xa) - length A < Suc nat
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length (remove1 e xa) - length A < Suc nat

goal (1 subgoal):
 1. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> list_order (remove1 e xa) x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (remove1 e xa) - length A < Suc nat

goal (1 subgoal):
 1. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> list_order (remove1 e xa) x y
[PROOF STEP]
have "insert_ops (remove1 e xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_ops (remove1 e xa)
[PROOF STEP]
by (simp add: insert_ops_remove1 less.prems(2))
[PROOF STATE]
proof (state)
this:
insert_ops (remove1 e xa)

goal (1 subgoal):
 1. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> list_order (remove1 e xa) x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert_ops (remove1 e xa)

goal (1 subgoal):
 1. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> list_order (remove1 e xa) x y
[PROOF STEP]
have "set A \<subseteq> set (remove1 e xa)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set A \<subseteq> set (remove1 e xa)
[PROOF STEP]
by (metis (no_types, lifting) \<open>e \<notin> set A\<close> in_set_remove1 less.prems(3) rev_subsetD subsetI)
[PROOF STATE]
proof (state)
this:
set A \<subseteq> set (remove1 e xa)

goal (1 subgoal):
 1. \<lbrakk>e \<in> set xa; e \<notin> set A\<rbrakk> \<Longrightarrow> list_order (remove1 e xa) x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (remove1 e xa) - length A < Suc nat
insert_ops (remove1 e xa)
set A \<subseteq> set (remove1 e xa)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length (remove1 e xa) - length A < Suc nat
insert_ops (remove1 e xa)
set A \<subseteq> set (remove1 e xa)

goal (1 subgoal):
 1. list_order (remove1 e xa) x y
[PROOF STEP]
by (simp add: Suc less.IH less.prems(1) less.prems(4))
[PROOF STATE]
proof (state)
this:
list_order (remove1 e xa) x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order (remove1 e xa) x y

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_order (remove1 e xa) x y
[PROOF STEP]
obtain xs ys zs where "interp_ins (remove1 e xa) = xs @ x # ys @ y # zs"
[PROOF STATE]
proof (prove)
using this:
list_order (remove1 e xa) x y

goal (1 subgoal):
 1. (\<And>xs ys zs. interp_ins (remove1 e xa) = xs @ x # ys @ y # zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using list_order_def
[PROOF STATE]
proof (prove)
using this:
list_order (remove1 e xa) x y
list_order ?ops ?x ?y \<equiv> \<exists>xs ys zs. interp_ins ?ops = xs @ [?x] @ ys @ [?y] @ zs

goal (1 subgoal):
 1. (\<And>xs ys zs. interp_ins (remove1 e xa) = xs @ x # ys @ y # zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
interp_ins (remove1 e xa) = xs @ x # ys @ y # zs

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (remove1 e xa) = xs @ x # ys @ y # zs

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
obtain oid ref where e_pair: "e = (oid, ref)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>oid ref. e = (oid, ref) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
e = (oid, ref)

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
e = (oid, ref)

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
obtain ps ss where xa_split: "xa = ps @ [e] @ ss" and "e \<notin> set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ps ss. \<lbrakk>xa = ps @ [e] @ ss; e \<notin> set ps\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using split_list_first \<open>e \<in> set xa\<close>
[PROOF STATE]
proof (prove)
using this:
?x \<in> set ?xs \<Longrightarrow> \<exists>ys zs. ?xs = ys @ ?x # zs \<and> ?x \<notin> set ys
e \<in> set xa

goal (1 subgoal):
 1. (\<And>ps ss. \<lbrakk>xa = ps @ [e] @ ss; e \<notin> set ps\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xa = ps @ [e] @ ss
e \<notin> set ps

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "remove1 e (ps @ e # ss) = ps @ ss"
[PROOF STATE]
proof (prove)
using this:
xa = ps @ [e] @ ss
e \<notin> set ps

goal (1 subgoal):
 1. remove1 e (ps @ e # ss) = ps @ ss
[PROOF STEP]
by (simp add: remove1_append)
[PROOF STATE]
proof (state)
this:
remove1 e (ps @ e # ss) = ps @ ss

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
remove1 e (ps @ e # ss) = ps @ ss

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
remove1 e (ps @ e # ss) = ps @ ss
[PROOF STEP]
have "insert_ops (ps @ ss)" and "insert_ops (ps @ e # ss)"
[PROOF STATE]
proof (prove)
using this:
remove1 e (ps @ e # ss) = ps @ ss

goal (1 subgoal):
 1. insert_ops (ps @ ss) &&& insert_ops (ps @ e # ss)
[PROOF STEP]
using xa_split less.prems(2)
[PROOF STATE]
proof (prove)
using this:
remove1 e (ps @ e # ss) = ps @ ss
xa = ps @ [e] @ ss
insert_ops xa

goal (1 subgoal):
 1. insert_ops (ps @ ss) &&& insert_ops (ps @ e # ss)
[PROOF STEP]
by (metis append_Cons append_Nil insert_ops_remove1, auto)
[PROOF STATE]
proof (state)
this:
insert_ops (ps @ ss)
insert_ops (ps @ e # ss)

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert_ops (ps @ ss)
insert_ops (ps @ e # ss)
[PROOF STEP]
obtain xsa ysa zsa where "interp_ins (ps @ ss) = xsa @ zsa"
      and interp_xa: "interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa"
[PROOF STATE]
proof (prove)
using this:
insert_ops (ps @ ss)
insert_ops (ps @ e # ss)

goal (1 subgoal):
 1. (\<And>xsa zsa ysa. \<lbrakk>interp_ins (ps @ ss) = xsa @ zsa; interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert_preserves_order e_pair
[PROOF STATE]
proof (prove)
using this:
insert_ops (ps @ ss)
insert_ops (ps @ e # ss)
\<lbrakk>insert_ops ?ops; insert_ops ?rest; ?rest = ?before @ ?after; ?ops = ?before @ (?oid, ?ref) # ?after\<rbrakk> \<Longrightarrow> \<exists>xs ys zs. interp_ins ?rest = xs @ zs \<and> interp_ins ?ops = xs @ ys @ zs
e = (oid, ref)

goal (1 subgoal):
 1. (\<And>xsa zsa ysa. \<lbrakk>interp_ins (ps @ ss) = xsa @ zsa; interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
interp_ins (ps @ ss) = xsa @ zsa
interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
interp_ins (ps @ ss) = xsa @ zsa
interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
have xsa_zsa: "xsa @ zsa = xs @ x # ys @ y # zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xsa @ zsa = xs @ x # ys @ y # zs
[PROOF STEP]
using interp_ins_def remove1_append calculation xa_split
[PROOF STATE]
proof (prove)
using this:
interp_ins ?ops \<equiv> foldl insert_spec [] ?ops
remove1 ?x (?xs @ ?ys) = (if ?x \<in> set ?xs then remove1 ?x ?xs @ ?ys else ?xs @ remove1 ?x ?ys)
interp_ins (remove1 e xa) = xs @ x # ys @ y # zs
e = (oid, ref)
remove1 e (ps @ e # ss) = ps @ ss
interp_ins (ps @ ss) = xsa @ zsa
interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa
xa = ps @ [e] @ ss

goal (1 subgoal):
 1. xsa @ zsa = xs @ x # ys @ y # zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xsa @ zsa = xs @ x # ys @ y # zs

goal (1 subgoal):
 1. \<And>nat. \<lbrakk>distinct A; distinct xa; length xa - length A = Suc nat\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xsa @ zsa = xs @ x # ys @ y # zs
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
xsa @ zsa = xs @ x # ys @ y # zs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
proof(cases "length xsa \<le> length xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xsa \<le> length xs

goal (2 subgoals):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xsa \<le> length xs
[PROOF STEP]
obtain ts where "xsa@ts = xs"
[PROOF STATE]
proof (prove)
using this:
length xsa \<le> length xs

goal (1 subgoal):
 1. (\<And>ts. xsa @ ts = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using app_length_lt_exists xsa_zsa
[PROOF STATE]
proof (prove)
using this:
length xsa \<le> length xs
\<lbrakk>?xsa @ ?zsa = ?xs @ ?ys; length ?xsa \<le> length ?xs\<rbrakk> \<Longrightarrow> ?xsa @ drop (length ?xsa) ?xs = ?xs
xsa @ zsa = xs @ x # ys @ y # zs

goal (1 subgoal):
 1. (\<And>ts. xsa @ ts = xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xsa @ ts = xs

goal (2 subgoals):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs"
[PROOF STATE]
proof (prove)
using this:
xsa @ ts = xs

goal (1 subgoal):
 1. interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs
[PROOF STEP]
using calculation xa_split
[PROOF STATE]
proof (prove)
using this:
xsa @ ts = xs
interp_ins (remove1 e xa) = xs @ x # ys @ y # zs
e = (oid, ref)
remove1 e (ps @ e # ss) = ps @ ss
interp_ins (ps @ ss) = xsa @ zsa
interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa
xa = ps @ [e] @ ss

goal (1 subgoal):
 1. interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs

goal (2 subgoals):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
using list_order_def
[PROOF STATE]
proof (prove)
using this:
interp_ins xa = (xsa @ ysa @ ts) @ [x] @ ys @ [y] @ zs
list_order ?ops ?x ?y \<equiv> \<exists>xs ys zs. interp_ins ?ops = xs @ [?x] @ ys @ [?y] @ zs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal (1 subgoal):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xsa \<le> length xs

goal (1 subgoal):
 1. \<lbrakk>xsa @ zsa = xs @ x # ys @ y # zs; \<not> length xsa \<le> length xs\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> length xsa \<le> length xs
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
\<not> length xsa \<le> length xs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
proof(cases "length xsa \<le> length (xs @ x # ys)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
length xsa \<le> length (xs @ x # ys)

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
have xsa_zsa1: "xsa @ zsa = (xs @ x # ys) @ (y # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xsa @ zsa = (xs @ x # ys) @ y # zs
[PROOF STEP]
by (simp add: xsa_zsa)
[PROOF STATE]
proof (state)
this:
xsa @ zsa = (xs @ x # ys) @ y # zs

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
xsa @ zsa = (xs @ x # ys) @ y # zs
[PROOF STEP]
obtain us where "xsa @ us = xs @ x # ys"
[PROOF STATE]
proof (prove)
using this:
xsa @ zsa = (xs @ x # ys) @ y # zs

goal (1 subgoal):
 1. (\<And>us. xsa @ us = xs @ x # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using app_length_lt_exists True
[PROOF STATE]
proof (prove)
using this:
xsa @ zsa = (xs @ x # ys) @ y # zs
\<lbrakk>?xsa @ ?zsa = ?xs @ ?ys; length ?xsa \<le> length ?xs\<rbrakk> \<Longrightarrow> ?xsa @ drop (length ?xsa) ?xs = ?xs
length xsa \<le> length (xs @ x # ys)

goal (1 subgoal):
 1. (\<And>us. xsa @ us = xs @ x # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xsa @ us = xs @ x # ys

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xsa @ us = xs @ x # ys

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
xsa @ us = xs @ x # ys
[PROOF STEP]
have "xs @ x # (drop (Suc (length xs)) xsa) = xsa"
[PROOF STATE]
proof (prove)
using this:
xsa @ us = xs @ x # ys

goal (1 subgoal):
 1. xs @ x # drop (Suc (length xs)) xsa = xsa
[PROOF STEP]
using append_eq_append_conv_if id_take_nth_drop linorder_not_less
            nth_append nth_append_length False
[PROOF STATE]
proof (prove)
using this:
xsa @ us = xs @ x # ys
(?xs\<^sub>1 @ ?xs\<^sub>2 = ?ys\<^sub>1 @ ?ys\<^sub>2) = (if length ?xs\<^sub>1 \<le> length ?ys\<^sub>1 then ?xs\<^sub>1 = take (length ?xs\<^sub>1) ?ys\<^sub>1 \<and> ?xs\<^sub>2 = drop (length ?xs\<^sub>1) ?ys\<^sub>1 @ ?ys\<^sub>2 else take (length ?ys\<^sub>1) ?xs\<^sub>1 = ?ys\<^sub>1 \<and> drop (length ?ys\<^sub>1) ?xs\<^sub>1 @ ?xs\<^sub>2 = ?ys\<^sub>2)
?i < length ?xs \<Longrightarrow> ?xs = take ?i ?xs @ ?xs ! ?i # drop (Suc ?i) ?xs
(\<not> ?x < ?y) = (?y \<le> ?x)
(?xs @ ?ys) ! ?n = (if ?n < length ?xs then ?xs ! ?n else ?ys ! (?n - length ?xs))
(?xs @ ?x # ?ys) ! length ?xs = ?x
\<not> length xsa \<le> length xs

goal (1 subgoal):
 1. xs @ x # drop (Suc (length xs)) xsa = xsa
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
xs @ x # drop (Suc (length xs)) xsa = xsa

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs @ x # drop (Suc (length xs)) xsa = xsa

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
have "us @ y # zs = zsa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us @ y # zs = zsa
[PROOF STEP]
by (metis True xsa_zsa1 append_eq_append_conv_if append_eq_conv_conj calculation(1))
[PROOF STATE]
proof (state)
this:
us @ y # zs = zsa

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xsa @ us = xs @ x # ys
xs @ x # drop (Suc (length xs)) xsa = xsa
us @ y # zs = zsa
[PROOF STEP]
have "interp_ins xa = xs @ [x] @
              ((drop (Suc (length xs)) xsa) @ ysa @ us) @ [y] @ zs"
[PROOF STATE]
proof (prove)
using this:
xsa @ us = xs @ x # ys
xs @ x # drop (Suc (length xs)) xsa = xsa
us @ y # zs = zsa

goal (1 subgoal):
 1. interp_ins xa = xs @ [x] @ (drop (Suc (length xs)) xsa @ ysa @ us) @ [y] @ zs
[PROOF STEP]
by (simp add: e_pair interp_xa xa_split)
[PROOF STATE]
proof (state)
this:
interp_ins xa = xs @ [x] @ (drop (Suc (length xs)) xsa @ ysa @ us) @ [y] @ zs

goal (2 subgoals):
 1. \<lbrakk>\<not> length xsa \<le> length xs; length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
 2. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins xa = xs @ [x] @ (drop (Suc (length xs)) xsa @ ysa @ us) @ [y] @ zs
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
interp_ins xa = xs @ [x] @ (drop (Suc (length xs)) xsa @ ysa @ us) @ [y] @ zs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
using list_order_def
[PROOF STATE]
proof (prove)
using this:
interp_ins xa = xs @ [x] @ (drop (Suc (length xs)) xsa @ ysa @ us) @ [y] @ zs
list_order ?ops ?x ?y \<equiv> \<exists>xs ys zs. interp_ins ?ops = xs @ [?x] @ ys @ [?y] @ zs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> length xsa \<le> length (xs @ x # ys)

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "length (xs @ x # ys) < length xsa"
[PROOF STATE]
proof (prove)
using this:
\<not> length xsa \<le> length (xs @ x # ys)

goal (1 subgoal):
 1. length (xs @ x # ys) < length xsa
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
\<not> length xsa \<le> length (xs @ x # ys)
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. length (xs @ x # ys) < length xsa
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length (xs @ x # ys) < length xsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "length (xs @ x # ys @ [y]) \<le> length xsa"
[PROOF STATE]
proof (prove)
using this:
length (xs @ x # ys) < length xsa

goal (1 subgoal):
 1. length (xs @ x # ys @ [y]) \<le> length xsa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (xs @ x # ys @ [y]) \<le> length xsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (xs @ x # ys @ [y]) \<le> length xsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
have "(xs @ x # ys @ [y]) @ zs = xsa @ zsa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (xs @ x # ys @ [y]) @ zs = xsa @ zsa
[PROOF STEP]
by (simp add: xsa_zsa)
[PROOF STATE]
proof (state)
this:
(xs @ x # ys @ [y]) @ zs = xsa @ zsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length (xs @ x # ys @ [y]) \<le> length xsa
(xs @ x # ys @ [y]) @ zs = xsa @ zsa
[PROOF STEP]
obtain vs where "(xs @ x # ys @ [y]) @ vs = xsa"
[PROOF STATE]
proof (prove)
using this:
length (xs @ x # ys @ [y]) \<le> length xsa
(xs @ x # ys @ [y]) @ zs = xsa @ zsa

goal (1 subgoal):
 1. (\<And>vs. (xs @ x # ys @ [y]) @ vs = xsa \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using app_length_lt_exists
[PROOF STATE]
proof (prove)
using this:
length (xs @ x # ys @ [y]) \<le> length xsa
(xs @ x # ys @ [y]) @ zs = xsa @ zsa
\<lbrakk>?xsa @ ?zsa = ?xs @ ?ys; length ?xsa \<le> length ?xs\<rbrakk> \<Longrightarrow> ?xsa @ drop (length ?xsa) ?xs = ?xs

goal (1 subgoal):
 1. (\<And>vs. (xs @ x # ys @ [y]) @ vs = xsa \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(xs @ x # ys @ [y]) @ vs = xsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "xsa @ ysa @ zsa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa"
[PROOF STATE]
proof (prove)
using this:
(xs @ x # ys @ [y]) @ vs = xsa

goal (1 subgoal):
 1. xsa @ ysa @ zsa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xsa @ ysa @ zsa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
hence "interp_ins xa = xs @ [x] @ ys @ [y] @ (vs @ ysa @ zsa)"
[PROOF STATE]
proof (prove)
using this:
xsa @ ysa @ zsa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa

goal (1 subgoal):
 1. interp_ins xa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa
[PROOF STEP]
using e_pair interp_xa xa_split
[PROOF STATE]
proof (prove)
using this:
xsa @ ysa @ zsa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa
e = (oid, ref)
interp_ins (ps @ (oid, ref) # ss) = xsa @ ysa @ zsa
xa = ps @ [e] @ ss

goal (1 subgoal):
 1. interp_ins xa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
interp_ins xa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa

goal (1 subgoal):
 1. \<lbrakk>\<not> length xsa \<le> length xs; \<not> length xsa \<le> length (xs @ x # ys)\<rbrakk> \<Longrightarrow> list_order xa x y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
interp_ins xa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa
[PROOF STEP]
show "list_order xa x y"
[PROOF STATE]
proof (prove)
using this:
interp_ins xa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
using list_order_def
[PROOF STATE]
proof (prove)
using this:
interp_ins xa = xs @ [x] @ ys @ [y] @ vs @ ysa @ zsa
list_order ?ops ?x ?y \<equiv> \<exists>xs ys zs. interp_ins ?ops = xs @ [?x] @ ys @ [?y] @ zs

goal (1 subgoal):
 1. list_order xa x y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_order xa x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_nonneg_nonneg [simp]:
  assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> a + b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) \<le> a + b
[PROOF STEP]
have "0 + 0 \<le> a + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) + (0::'a) \<le> a + b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> a
(0::'a) \<le> b

goal (1 subgoal):
 1. (0::'a) + (0::'a) \<le> a + b
[PROOF STEP]
by (rule add_mono)
[PROOF STATE]
proof (state)
this:
(0::'a) + (0::'a) \<le> a + b

goal (1 subgoal):
 1. (0::'a) \<le> a + b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(0::'a) + (0::'a) \<le> a + b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(0::'a) + (0::'a) \<le> a + b

goal (1 subgoal):
 1. (0::'a) \<le> a + b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> a + b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_nonpos_nonpos[simp]:
  assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b \<le> (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a + b \<le> (0::'a)
[PROOF STEP]
have "a + b \<le> 0 + 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b \<le> (0::'a) + (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<le> (0::'a)
b \<le> (0::'a)

goal (1 subgoal):
 1. a + b \<le> (0::'a) + (0::'a)
[PROOF STEP]
by (rule add_mono)
[PROOF STATE]
proof (state)
this:
a + b \<le> (0::'a) + (0::'a)

goal (1 subgoal):
 1. a + b \<le> (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a + b \<le> (0::'a) + (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a + b \<le> (0::'a) + (0::'a)

goal (1 subgoal):
 1. a + b \<le> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a + b \<le> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_nonneg_eq_0_iff:
  assumes x: "0 \<le> x" and y: "0 \<le> y"
  shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + y = (0::'a)) = (x = (0::'a) \<and> y = (0::'a))
[PROOF STEP]
by (metis local.add_0_left local.add_0_right local.add_left_mono local.antisym_conv x y)


[STATEMENT]
lemma add_incr: "0\<le>b \<Longrightarrow> a \<le> a+b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> b \<Longrightarrow> a \<le> a + b
[PROOF STEP]
by (metis add.comm_neutral add_left_mono)


[STATEMENT]
lemma add_incr_left[simp, intro!]: "0\<le>b \<Longrightarrow> a \<le> b + a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> b \<Longrightarrow> a \<le> b + a
[PROOF STEP]
by (metis add_incr add.commute)


[STATEMENT]
lemma sum_not_less[simp, intro!]:
  "0\<le>b \<Longrightarrow> \<not> (a+b < a)"
  "0\<le>a \<Longrightarrow> \<not> (a+b < b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((0::'a) \<le> b \<Longrightarrow> \<not> a + b < a) &&& ((0::'a) \<le> a \<Longrightarrow> \<not> a + b < b)
[PROOF STEP]
apply (metis add_incr less_le_not_le)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> a \<Longrightarrow> \<not> a + b < b
[PROOF STEP]
apply (metis add_incr_left less_le_not_le)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma inf_add_left[simp]: "top + a = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top + a = top
[PROOF STEP]
by (metis add.commute inf_add_right)


[STATEMENT]
lemma not_less_inf[simp]:
  "\<not> (a < top) \<longleftrightarrow> a=top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> a < top) = (a = top)
[PROOF STEP]
by simp


[STATEMENT]
lemma num_val_iff[simp]: "e\<noteq>Infty \<Longrightarrow> Num (val e) = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<noteq> Infty \<Longrightarrow> Num (val e) = e
[PROOF STEP]
by (cases e) auto


[STATEMENT]
lemma [simp]: "Infty\<le>a \<longleftrightarrow> a=Infty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Infty \<le> a) = (a = Infty)
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma [simp]: "less a Infty \<longleftrightarrow> a \<noteq> Infty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a < Infty) = (a \<noteq> Infty)
[PROOF STEP]
by (cases a) auto


[STATEMENT]
lemma [simp]: "plus Infty a = Infty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Infty + a = Infty
[PROOF STEP]
by (cases a) simp_all


[STATEMENT]
lemma infty_inf_unbox:
  "Num a \<noteq> top"
  "top \<noteq> Num a"
  "Infty = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Num a \<noteq> top &&& top \<noteq> Num a &&& Infty = top
[PROOF STEP]
by (auto simp add: top_infty_def)


[STATEMENT]
lemma infty_ord_unbox:
  "Num a \<le> Num b \<longleftrightarrow> a \<le> b"
  "Num a < Num b \<longleftrightarrow> a < b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Num a \<le> Num b) = (a \<le> b) &&& (Num a < Num b) = (a < b)
[PROOF STEP]
by auto


[STATEMENT]
lemma infty_plus_unbox:
  "Num a + Num b = Num (a+b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Num a + Num b = Num (a + b)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma infty_zero_unbox:
  "Num a = 0 \<longleftrightarrow> a = 0"
  "Num 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Num a = 0) = (a = (0::'a)) &&& Num (0::'b) = 0
[PROOF STEP]
by (auto simp: zero_infty_def)


[STATEMENT]
lemma inf_not_zero[simp]:
  "top\<noteq>(0::_ infty)" "(0::_ infty)\<noteq>top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top \<noteq> 0 &&& 0 \<noteq> top
[PROOF STEP]
apply (unfold zero_infty_def top_infty_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Infty \<noteq> Num (0::'a)
 2. Num (0::'b) \<noteq> Infty
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma num_val_iff'[simp]: "e\<noteq>top \<Longrightarrow> Num (val e) = e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e \<noteq> top \<Longrightarrow> Num (val e) = e
[PROOF STEP]
by (cases e) (auto simp add: infty_unbox)


[STATEMENT]
lemma infty_neE:
  "\<lbrakk>a\<noteq>Infty; \<And>d. a=Num d \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
  "\<lbrakk>a\<noteq>top; \<And>d. a=Num d \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a \<noteq> Infty; \<And>d. a = Num d \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P) &&& (\<lbrakk>a \<noteq> top; \<And>d. a = Num d \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P)
[PROOF STEP]
by (case_tac [!] a) (auto simp add: infty_unbox)


[STATEMENT]
lemma sym_preproc_aux_term1_wf_on:
  assumes "dickson_grading d"
  shows "wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
proof (rule wfp_onI_min)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
let ?B = "pp_of_term -` dgrad_set d m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
let ?A = "{x::(('t \<Rightarrow>\<^sub>0 'b) list \<times> 't list \<times> 't list \<times> ('t \<Rightarrow>\<^sub>0 'b) list). set (fst (snd (snd x))) \<subseteq> ?B}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
have A_sub_Pow: "set ` fst ` snd ` snd ` ?A \<subseteq> Pow ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ` fst ` snd ` snd ` {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m} \<subseteq> Pow (pp_of_term -` dgrad_set d m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ` fst ` snd ` snd ` {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m} \<subseteq> Pow (pp_of_term -` dgrad_set d m)

goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
fix x Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
assume "x \<in> Q" and "Q \<subseteq> ?A"
[PROOF STATE]
proof (state)
this:
x \<in> Q
Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
let ?Q = "{ord_term_lin.Max (set (fst (snd (snd q)))) | q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. \<lbrakk>x \<in> Q; Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
show "\<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> ?B}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
proof (cases "\<exists>z\<in>Q. fst (snd (snd z)) = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>z\<in>Q. fst (snd (snd z)) = [] \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
 2. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Q. fst (snd (snd z)) = []

goal (2 subgoals):
 1. \<exists>z\<in>Q. fst (snd (snd z)) = [] \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
 2. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z\<in>Q. fst (snd (snd z)) = []
[PROOF STEP]
obtain z where "z \<in> Q" and "fst (snd (snd z)) = []"
[PROOF STATE]
proof (prove)
using this:
\<exists>z\<in>Q. fst (snd (snd z)) = []

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> Q; fst (snd (snd z)) = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
z \<in> Q
fst (snd (snd z)) = []

goal (2 subgoals):
 1. \<exists>z\<in>Q. fst (snd (snd z)) = [] \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
 2. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
proof (intro bexI ballI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d\<rbrakk> \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d\<rbrakk> \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
assume "(y, z) \<in> sym_preproc_aux_term1 d"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> sym_preproc_aux_term1 d

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d\<rbrakk> \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> sym_preproc_aux_term1 d
[PROOF STEP]
obtain t where "t \<in> set (fst (snd (snd z)))"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> sym_preproc_aux_term1 d

goal (1 subgoal):
 1. (\<And>t. t \<in> set (fst (snd (snd z))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sym_preproc_aux_term1_def
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> {((gs1, ks1, ts1, fs1), gs2, ks2, ts2, fs2). \<exists>t2\<in>set ts2. \<forall>t1\<in>set ts1. t1 \<prec>\<^sub>t t2}

goal (1 subgoal):
 1. (\<And>t. t \<in> set (fst (snd (snd z))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> set (fst (snd (snd z)))

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d\<rbrakk> \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
with \<open>fst (snd (snd z)) = []\<close>
[PROOF STATE]
proof (chain)
picking this:
fst (snd (snd z)) = []
t \<in> set (fst (snd (snd z)))
[PROOF STEP]
show "y \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
fst (snd (snd z)) = []
t \<in> set (fst (snd (snd z)))

goal (1 subgoal):
 1. y \<notin> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<notin> Q

goal (1 subgoal):
 1. z \<in> Q
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>z\<in>Q. fst (snd (snd z)) = [])

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
hence *: "q \<in> Q \<Longrightarrow> fst (snd (snd q)) \<noteq> []" for q
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>z\<in>Q. fst (snd (snd z)) = [])

goal (1 subgoal):
 1. q \<in> Q \<Longrightarrow> fst (snd (snd q)) \<noteq> []
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?q94 \<in> Q \<Longrightarrow> fst (snd (snd ?q94)) \<noteq> []

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
with \<open>x \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> Q
?q94 \<in> Q \<Longrightarrow> fst (snd (snd ?q94)) \<noteq> []
[PROOF STEP]
have "fst (snd (snd x)) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
x \<in> Q
?q94 \<in> Q \<Longrightarrow> fst (snd (snd ?q94)) \<noteq> []

goal (1 subgoal):
 1. fst (snd (snd x)) \<noteq> []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (snd (snd x)) \<noteq> []

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "wfp_on (\<prec>\<^sub>t) ?B"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)
[PROOF STEP]
by (rule wfp_on_ord_term_strict)
[PROOF STATE]
proof (state)
this:
wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from \<open>x \<in> Q\<close> \<open>fst (snd (snd x)) \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<in> Q
fst (snd (snd x)) \<noteq> []
[PROOF STEP]
have "ord_term_lin.Max (set (fst (snd (snd x)))) \<in> ?Q"
[PROOF STATE]
proof (prove)
using this:
x \<in> Q
fst (snd (snd x)) \<noteq> []

goal (1 subgoal):
 1. ord_term_lin.Max (set (fst (snd (snd x)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd x)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd x)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
have "?Q \<subseteq> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []} \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
proof (rule, simp, elim exE conjE, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
fix a b c d0
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
assume "(a, b, c, d0) \<in> Q" and "c \<noteq> []"
[PROOF STATE]
proof (state)
this:
(a, b, c, d0) \<in> Q
c \<noteq> []

goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
from this(1) \<open>Q \<subseteq> ?A\<close>
[PROOF STATE]
proof (chain)
picking this:
(a, b, c, d0) \<in> Q
Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
have "(a, b, c, d0) \<in> ?A"
[PROOF STATE]
proof (prove)
using this:
(a, b, c, d0) \<in> Q
Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. (a, b, c, d0) \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(a, b, c, d0) \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
hence "pp_of_term ` set c \<subseteq> dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
(a, b, c, d0) \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. pp_of_term ` set c \<subseteq> dgrad_set d m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pp_of_term ` set c \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pp_of_term ` set c \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
have "pp_of_term (ord_term_lin.Max (set c)) \<in> pp_of_term ` set c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pp_of_term (ord_term_lin.Max (set c)) \<in> pp_of_term ` set c
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pp_of_term (ord_term_lin.Max (set c)) = pp_of_term ?x
 2. ?x \<in> set c
[PROOF STEP]
from \<open>c \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> []
[PROOF STEP]
show "ord_term_lin.Max (set c) \<in> set c"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> []

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

goal (1 subgoal):
 1. pp_of_term (ord_term_lin.Max (set c)) = pp_of_term (ord_term_lin.Max (set c))
[PROOF STEP]
qed (fact refl)
[PROOF STATE]
proof (state)
this:
pp_of_term (ord_term_lin.Max (set c)) \<in> pp_of_term ` set c

goal (1 subgoal):
 1. \<And>x a aa ab b. \<lbrakk>x = ord_term_lin.Max (set ab); ab \<noteq> []; (a, aa, ab, b) \<in> Q\<rbrakk> \<Longrightarrow> pp_of_term (ord_term_lin.Max (set ab)) \<in> dgrad_set d m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pp_of_term ` set c \<subseteq> dgrad_set d m
pp_of_term (ord_term_lin.Max (set c)) \<in> pp_of_term ` set c
[PROOF STEP]
show "pp_of_term (ord_term_lin.Max (set c)) \<in> dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
pp_of_term ` set c \<subseteq> dgrad_set d m
pp_of_term (ord_term_lin.Max (set c)) \<in> pp_of_term ` set c

goal (1 subgoal):
 1. pp_of_term (ord_term_lin.Max (set c)) \<in> dgrad_set d m
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
pp_of_term (ord_term_lin.Max (set c)) \<in> dgrad_set d m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []} \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)
ord_term_lin.Max (set (fst (snd (snd x)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
{ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []} \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
obtain t where "t \<in> ?Q" and min: "\<And>s. s \<prec>\<^sub>t t \<Longrightarrow> s \<notin> ?Q"
[PROOF STATE]
proof (prove)
using this:
wfp_on (\<prec>\<^sub>t) (pp_of_term -` dgrad_set d m)
ord_term_lin.Max (set (fst (snd (snd x)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
{ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []} \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>t \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}; \<And>s. s \<prec>\<^sub>t t \<Longrightarrow> s \<notin> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule wfp_onE_min) blast
[PROOF STATE]
proof (state)
this:
t \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
?s94 \<prec>\<^sub>t t \<Longrightarrow> ?s94 \<notin> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
t \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
[PROOF STEP]
obtain z where "z \<in> Q" and "fst (snd (snd z)) \<noteq> []"
      and t: "t = ord_term_lin.Max (set (fst (snd (snd z))))"
[PROOF STATE]
proof (prove)
using this:
t \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> Q; fst (snd (snd z)) \<noteq> []; t = ord_term_lin.Max (set (fst (snd (snd z))))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> Q
fst (snd (snd z)) \<noteq> []
t = ord_term_lin.Max (set (fst (snd (snd z))))

goal (1 subgoal):
 1. \<not> (\<exists>z\<in>Q. fst (snd (snd z)) = []) \<Longrightarrow> \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q
[PROOF STEP]
proof (intro bexI ballI impI, rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
assume "y \<in> ?A" and "(y, z) \<in> sym_preproc_aux_term1 d" and "y \<in> Q"
[PROOF STATE]
proof (state)
this:
y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
(y, z) \<in> sym_preproc_aux_term1 d
y \<in> Q

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> sym_preproc_aux_term1 d
[PROOF STEP]
obtain t' where "t' \<in> set (fst (snd (snd z)))"
        and **: "\<And>s. s \<in> set (fst (snd (snd y))) \<Longrightarrow> s \<prec>\<^sub>t t'"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> sym_preproc_aux_term1 d

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<in> set (fst (snd (snd z))); \<And>s. s \<in> set (fst (snd (snd y))) \<Longrightarrow> s \<prec>\<^sub>t t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding sym_preproc_aux_term1_def
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> {((gs1, ks1, ts1, fs1), gs2, ks2, ts2, fs2). \<exists>t2\<in>set ts2. \<forall>t1\<in>set ts1. t1 \<prec>\<^sub>t t2}

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<in> set (fst (snd (snd z))); \<And>s. s \<in> set (fst (snd (snd y))) \<Longrightarrow> s \<prec>\<^sub>t t'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t' \<in> set (fst (snd (snd z)))
?s94 \<in> set (fst (snd (snd y))) \<Longrightarrow> ?s94 \<prec>\<^sub>t t'

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
from \<open>y \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> Q
[PROOF STEP]
have "fst (snd (snd y)) \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
y \<in> Q

goal (1 subgoal):
 1. fst (snd (snd y)) \<noteq> []
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
fst (snd (snd y)) \<noteq> []

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
with \<open>y \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<in> Q
fst (snd (snd y)) \<noteq> []
[PROOF STEP]
have "ord_term_lin.Max (set (fst (snd (snd y)))) \<in> ?Q" (is "?s \<in> _")
[PROOF STATE]
proof (prove)
using this:
y \<in> Q
fst (snd (snd y)) \<noteq> []

goal (1 subgoal):
 1. ord_term_lin.Max (set (fst (snd (snd y)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
from \<open>fst (snd (snd y)) \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
fst (snd (snd y)) \<noteq> []
[PROOF STEP]
have "?s \<in> set (fst (snd (snd y)))"
[PROOF STATE]
proof (prove)
using this:
fst (snd (snd y)) \<noteq> []

goal (1 subgoal):
 1. ord_term_lin.Max (set (fst (snd (snd y)))) \<in> set (fst (snd (snd y)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<in> set (fst (snd (snd y)))

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
hence "?s \<prec>\<^sub>t t'"
[PROOF STATE]
proof (prove)
using this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<in> set (fst (snd (snd y)))

goal (1 subgoal):
 1. ord_term_lin.Max (set (fst (snd (snd y)))) \<prec>\<^sub>t t'
[PROOF STEP]
by (rule **)
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<prec>\<^sub>t t'

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<prec>\<^sub>t t'

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
from \<open>t' \<in> set (fst (snd (snd z)))\<close>
[PROOF STATE]
proof (chain)
picking this:
t' \<in> set (fst (snd (snd z)))
[PROOF STEP]
have "t' \<preceq>\<^sub>t t"
[PROOF STATE]
proof (prove)
using this:
t' \<in> set (fst (snd (snd z)))

goal (1 subgoal):
 1. t' \<preceq>\<^sub>t t
[PROOF STEP]
unfolding t
[PROOF STATE]
proof (prove)
using this:
t' \<in> set (fst (snd (snd z)))

goal (1 subgoal):
 1. t' \<preceq>\<^sub>t ord_term_lin.Max (set (fst (snd (snd z))))
[PROOF STEP]
using \<open>fst (snd (snd z)) \<noteq> []\<close>
[PROOF STATE]
proof (prove)
using this:
t' \<in> set (fst (snd (snd z)))
fst (snd (snd z)) \<noteq> []

goal (1 subgoal):
 1. t' \<preceq>\<^sub>t ord_term_lin.Max (set (fst (snd (snd z))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t' \<preceq>\<^sub>t t

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<prec>\<^sub>t t
[PROOF STEP]
have "?s \<notin> ?Q"
[PROOF STATE]
proof (prove)
using this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<prec>\<^sub>t t

goal (1 subgoal):
 1. ord_term_lin.Max (set (fst (snd (snd y)))) \<notin> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
[PROOF STEP]
by (rule min)
[PROOF STATE]
proof (state)
this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<notin> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

goal (2 subgoals):
 1. \<And>y. \<lbrakk>y \<in> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}; (y, ?z) \<in> sym_preproc_aux_term1 d; y \<in> Q\<rbrakk> \<Longrightarrow> False
 2. ?z \<in> Q
[PROOF STEP]
from this \<open>?s \<in> ?Q\<close>
[PROOF STATE]
proof (chain)
picking this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<notin> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
ord_term_lin.Max (set (fst (snd (snd y)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
ord_term_lin.Max (set (fst (snd (snd y)))) \<notin> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}
ord_term_lin.Max (set (fst (snd (snd y)))) \<in> {ord_term_lin.Max (set (fst (snd (snd q)))) |q. q \<in> Q \<and> fst (snd (snd q)) \<noteq> []}

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

goal (1 subgoal):
 1. z \<in> Q
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Q. \<forall>y\<in>{x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}. (y, z) \<in> sym_preproc_aux_term1 d \<longrightarrow> y \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sym_preproc_aux_term_wf:
  assumes "dickson_grading d"
  shows "wf (sym_preproc_aux_term d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (sym_preproc_aux_term d)
[PROOF STEP]
proof (rule wfI_min)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
fix x::"(('t \<Rightarrow>\<^sub>0 'b) list \<times> 't list \<times> 't list \<times> ('t \<Rightarrow>\<^sub>0 'b) list)" and Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
assume "x \<in> Q"
[PROOF STATE]
proof (state)
this:
x \<in> Q

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
let ?A = "Keys (set (fst x)) \<union> set (fst (snd (snd x)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
have "finite ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (Keys (set (fst x)) \<union> set (fst (snd (snd x))))
[PROOF STEP]
by (simp add: finite_Keys)
[PROOF STATE]
proof (state)
this:
finite (Keys (set (fst x)) \<union> set (fst (snd (snd x))))

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
hence "finite (pp_of_term ` ?A)"
[PROOF STATE]
proof (prove)
using this:
finite (Keys (set (fst x)) \<union> set (fst (snd (snd x))))

goal (1 subgoal):
 1. finite (pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))))
[PROOF STEP]
by (rule finite_imageI)
[PROOF STATE]
proof (state)
this:
finite (pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))))

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))))
[PROOF STEP]
obtain m where "pp_of_term ` ?A \<subseteq> dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
finite (pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))))

goal (1 subgoal):
 1. (\<And>m. pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))) \<subseteq> dgrad_set d m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule dgrad_set_exhaust)
[PROOF STATE]
proof (state)
this:
pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))) \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
hence A: "?A \<subseteq> pp_of_term -` dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
pp_of_term ` (Keys (set (fst x)) \<union> set (fst (snd (snd x)))) \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. Keys (set (fst x)) \<union> set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Keys (set (fst x)) \<union> set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
let ?B = "pp_of_term -` dgrad_set d m"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
let ?Q = "{q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> ?B}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
dickson_grading d
[PROOF STEP]
have "wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> ?B}"
[PROOF STATE]
proof (prove)
using this:
dickson_grading d

goal (1 subgoal):
 1. wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
by (rule sym_preproc_aux_term1_wf_on)
[PROOF STATE]
proof (state)
this:
wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from \<open>x \<in> Q\<close> A
[PROOF STATE]
proof (chain)
picking this:
x \<in> Q
Keys (set (fst x)) \<union> set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
have "x \<in> ?Q"
[PROOF STATE]
proof (prove)
using this:
x \<in> Q
Keys (set (fst x)) \<union> set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. x \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
have "?Q \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> ?B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m} \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m} \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
x \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
{q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m} \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
obtain z where "z \<in> ?Q"
    and *: "\<And>y. (y, z) \<in> sym_preproc_aux_term1 d \<Longrightarrow> y \<notin> ?Q"
[PROOF STATE]
proof (prove)
using this:
wfp_on (\<lambda>x y. (x, y) \<in> sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}
x \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
{q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m} \<subseteq> {x. set (fst (snd (snd x))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}; \<And>y. (y, z) \<in> sym_preproc_aux_term1 d \<Longrightarrow> y \<notin> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule wfp_onE_min) blast
[PROOF STATE]
proof (state)
this:
z \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
(?y95, z) \<in> sym_preproc_aux_term1 d \<Longrightarrow> ?y95 \<notin> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from this(1)
[PROOF STATE]
proof (chain)
picking this:
z \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
have "z \<in> Q" and "Keys (set (fst z)) \<union> set (fst (snd (snd z))) \<subseteq> ?B"
[PROOF STATE]
proof (prove)
using this:
z \<in> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. z \<in> Q &&& Keys (set (fst z)) \<union> set (fst (snd (snd z))) \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
z \<in> Q
Keys (set (fst z)) \<union> set (fst (snd (snd z))) \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
Keys (set (fst z)) \<union> set (fst (snd (snd z))) \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
have a: "pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))) \<subseteq> dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
Keys (set (fst z)) \<union> set (fst (snd (snd z))) \<subseteq> pp_of_term -` dgrad_set d m

goal (1 subgoal):
 1. pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))) \<subseteq> dgrad_set d m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))) \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. \<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q
[PROOF STEP]
proof (intro bexI allI impI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
assume "(y, z) \<in> sym_preproc_aux_term d"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> sym_preproc_aux_term d

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
hence "(y, z) \<in> sym_preproc_aux_term1 d" and "(y, z) \<in> sym_preproc_aux_term2 d"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> sym_preproc_aux_term d

goal (1 subgoal):
 1. (y, z) \<in> sym_preproc_aux_term1 d &&& (y, z) \<in> sym_preproc_aux_term2 d
[PROOF STEP]
by (simp_all add: sym_preproc_aux_term_def)
[PROOF STATE]
proof (state)
this:
(y, z) \<in> sym_preproc_aux_term1 d
(y, z) \<in> sym_preproc_aux_term2 d

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> sym_preproc_aux_term2 d
[PROOF STEP]
have "fst y = fst z"
      and "dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))))"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> sym_preproc_aux_term2 d

goal (1 subgoal):
 1. fst y = fst z &&& dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))))
[PROOF STEP]
by (auto simp add: sym_preproc_aux_term2_def)
[PROOF STATE]
proof (state)
this:
fst y = fst z
dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))))

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
from this(2) a
[PROOF STATE]
proof (chain)
picking this:
dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))))
pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))) \<subseteq> dgrad_set d m
[PROOF STEP]
have "pp_of_term ` (set (fst (snd (snd y)))) \<subseteq> dgrad_set d m"
[PROOF STATE]
proof (prove)
using this:
dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))))
pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))) \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. pp_of_term ` set (fst (snd (snd y))) \<subseteq> dgrad_set d m
[PROOF STEP]
by (rule dgrad_set_le_dgrad_set)
[PROOF STATE]
proof (state)
this:
pp_of_term ` set (fst (snd (snd y))) \<subseteq> dgrad_set d m

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
hence "Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> ?B"
[PROOF STATE]
proof (prove)
using this:
pp_of_term ` set (fst (snd (snd y))) \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
pp_of_term ` set (fst (snd (snd y))) \<subseteq> dgrad_set d m
pp_of_term ` (Keys (set (fst z)) \<union> set (fst (snd (snd z)))) \<subseteq> dgrad_set d m

goal (1 subgoal):
 1. Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> pp_of_term -` dgrad_set d m
[PROOF STEP]
by (auto simp add: \<open>fst y = fst z\<close>)
[PROOF STATE]
proof (state)
this:
Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> pp_of_term -` dgrad_set d m

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> pp_of_term -` dgrad_set d m

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
from \<open>(y, z) \<in> sym_preproc_aux_term1 d\<close>
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> sym_preproc_aux_term1 d
[PROOF STEP]
have "y \<notin> ?Q"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> sym_preproc_aux_term1 d

goal (1 subgoal):
 1. y \<notin> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
by (rule *)
[PROOF STATE]
proof (state)
this:
y \<notin> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (2 subgoals):
 1. \<And>y. (y, ?z) \<in> sym_preproc_aux_term d \<Longrightarrow> y \<notin> Q
 2. ?z \<in> Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> pp_of_term -` dgrad_set d m
y \<notin> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}
[PROOF STEP]
show "y \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
Keys (set (fst y)) \<union> set (fst (snd (snd y))) \<subseteq> pp_of_term -` dgrad_set d m
y \<notin> {q \<in> Q. Keys (set (fst q)) \<union> set (fst (snd (snd q))) \<subseteq> pp_of_term -` dgrad_set d m}

goal (1 subgoal):
 1. y \<notin> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<notin> Q

goal (1 subgoal):
 1. z \<in> Q
[PROOF STEP]
qed fact
[PROOF STATE]
proof (state)
this:
\<exists>z\<in>Q. \<forall>y. (y, z) \<in> sym_preproc_aux_term d \<longrightarrow> y \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed