Theory Decreasing_Diagrams

(*  Title:       Formalization of Decreasing Diagrams
    Author:      Harald Zankl  <Harald.Zankl at uibk.ac.at>, 2012
    Maintainer:  Harald Zankl  <Harald.Zankl at uibk.ac.at>, 2013
*)

(*
Copyright 2012 Harald Zankl

This formalization is free software: you can redistribute it and/or modify it under
the terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later version.

This formalization is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with the formalization. If not, see <http://www.gnu.org/licenses/>.
*)

section "Decreasing Diagrams"


theory Decreasing_Diagrams imports "HOL-Library.Multiset" "Abstract-Rewriting.Abstract_Rewriting" begin

subsection  Valley Version

text This section follows~\cite{vO94}.

subsubsection Appendix

text interaction of multisets with sets
definition diff :: "'a multiset  'a set  'a multiset"
 where "diff M S = filter_mset (λx. x  S) M"

definition intersect :: "'a multiset  'a set  'a multiset"
 where "intersect M S = filter_mset (λx. x  S) M"

notation
 diff      (infixl "-s" 800) and
 intersect (infixl "∩s" 800)

lemma count_diff [simp]:
  "count (M -s A) a = count M a * of_bool (a  A)"
  by (simp add: diff_def)

lemma set_mset_diff [simp]:
  "set_mset (M -s A) = set_mset M - A"
  by (auto simp add: diff_def)

lemma diff_eq_singleton_imp:
  "M -s A = {#a#}  a  (set_mset M - A)"
  unfolding diff_def filter_mset_eq_conv by auto

lemma count_intersect [simp]:
  "count (M ∩s A) a = count M a * of_bool (a  A)"
  by (simp add: intersect_def)

lemma set_mset_intersect [simp]:
  "set_mset (M ∩s A) = set_mset M  A"
  by (auto simp add: intersect_def)

lemma diff_from_empty: "{#}-s S = {#}" unfolding diff_def by auto

lemma diff_empty: "M -s {} = M" unfolding diff_def by (rule multiset_eqI) simp

lemma submultiset_implies_subset: assumes "M ⊆# N" shows "set_mset M  set_mset N"
 using assms mset_subset_eqD by auto

lemma subset_implies_remove_empty: assumes "set_mset M  S" shows "M -s S = {#}"
 unfolding diff_def using assms by (induct M) auto

lemma remove_empty_implies_subset: assumes "M -s S = {#}" shows "set_mset M  S" proof
 fix x assume A: "x  set_mset M"
 have "x  set_mset (M -s S)" using assms by auto
 thus "x  S" using A unfolding diff_def by auto
qed

lemma lemmaA_3_8:  "(M + N) -s S = (M -s S) + (N -s S)" unfolding diff_def by (rule multiset_eqI) simp
lemma lemmaA_3_9:  "(M -s S) -s T = M -s (S  T)" unfolding diff_def by (rule multiset_eqI) simp
lemma lemmaA_3_10: "M = (M ∩s S) + (M -s S)" unfolding diff_def intersect_def by auto
lemma lemmaA_3_11: "(M -s T) ∩s S = (M ∩s S) -s T" unfolding diff_def intersect_def by (rule multiset_eqI) simp

subsubsection Multisets
text Definition 2.5(1)
definition ds :: "'a rel  'a set  'a set"
 where "ds r S = {y . x  S. (y,x)  r}"

definition dm :: "'a rel  'a multiset  'a set"
 where "dm r M = ds r (set_mset M)"

definition dl :: "'a rel  'a list  'a set"
 where "dl r σ = ds r (set σ)"

notation
 ds (infixl "↓s" 900) and
 dm (infixl "↓m" 900) and
 dl (infixl "↓l" 900)

text missing but useful
lemma ds_ds_subseteq_ds: assumes t: "trans r" shows "ds r (ds r S)  ds r S" proof
 fix x assume A: "x  ds r (ds r S)" show "x  ds r S" proof -
  from A obtain y z where "(x,y)  r" and "(y,z)  r" and mem: "z  S" unfolding ds_def by auto
  thus ?thesis using mem t trans_def unfolding ds_def by fast
 qed
qed

text from PhD thesis of van Oostrom
lemma ds_monotone: assumes "S  T" shows "ds r S  ds r T" using assms unfolding ds_def by auto

lemma subset_imp_ds_subset: assumes "trans r" and "S  ds r T" shows "ds r S  ds r T"
 using assms ds_monotone ds_ds_subseteq_ds by blast

text Definition 2.5(2)

text strict order (mult) is used from Multiset.thy
definition mult_eq :: "'a rel  'a multiset rel" where
  "mult_eq r = (mult1 r)*"

definition mul :: "'a rel  'a multiset rel" where
  "mul r = {(M,N).I J K. M = I + K  N = I + J  set_mset K  dm r J  J  {#}}"

definition mul_eq :: "'a rel  'a multiset rel" where
  "mul_eq r = {(M,N).I J K. M = I + K  N = I + J  set_mset K  dm r J}"

lemma in_mul_eqI:
  assumes "M = I + K" "N = I + J" "set_mset K  r ↓m J"
  shows "(M, N)  mul_eq r"
  using assms by (auto simp add: mul_eq_def)

lemma downset_intro:
assumes "kset_mset K.jset_mset J.(k,j)r" shows "set_mset K  dm r J" proof
 fix x assume "xset_mset K" thus "x  dm r J" using assms unfolding dm_def ds_def by fast
qed

lemma downset_elim:
assumes "set_mset K  dm r J" shows "kset_mset K.jset_mset J.(k,j)r" proof
 fix k assume "k set_mset K" thus "jset_mset J.(k,j) r" using assms unfolding dm_def ds_def by fast
qed

text to closure-free representation
lemma mult_eq_implies_one_or_zero_step:
assumes "trans r" and "(M,N)  mult_eq r" shows "I J K. N = I + J  M = I + K  set_mset K  dm r J"
proof (cases "(M,N)  mult r")
  case True thus ?thesis using mult_implies_one_step[OF assms(1)] downset_intro by blast
 next
  case False hence A: "M = N" using assms rtrancl_eq_or_trancl unfolding mult_eq_def mult_def by metis
  hence "N = N + {#}  M = M + {#}  set_mset {#}  dm r{#}" by auto
  thus ?thesis unfolding A by fast
qed

text from closure-free representation
lemma one_step_implies_mult_eq: assumes "trans r" and "set_mset K  dm r J" shows "(I+K,I+J)mult_eq r"
proof (cases "set_mset J = {}")
 case True hence "set_mset K = {}" using assms downset_elim by (metis all_not_in_conv emptyE)
 thus ?thesis using True unfolding mult_eq_def by auto
next
 case False hence h:"J  {#}" using set_mset_eq_empty_iff by auto
  hence "(I+K,I+J) mult r" using set_mset_eq_empty_iff assms one_step_implies_mult downset_elim
    by auto blast
  thus ?thesis unfolding mult_eq_def mult_def by auto
qed

lemma mult_is_mul: assumes "trans r" shows "mult r = mul r" proof
 show "mult r  mul r" proof
  fix N M assume A: "(N,M)  mult r" show "(N,M)  mul r" proof -
   obtain I J K where "M = I + J" and "N = I + K" and "J  {#}" and "set_mset K  dm r J"
    using mult_implies_one_step[OF assms A] downset_intro by metis
   thus ?thesis unfolding mul_def by auto
  qed
 qed
 next
 show "mul r  mult r" proof
  fix N M assume A: "(N,M)  mul r" show "(N,M)  mult r" proof -
   obtain I J K where "M = I + J" and "N = I + K" and "J  {#}" and "set_mset K  dm r J"
    using A unfolding mul_def by auto
   thus ?thesis using one_step_implies_mult assms downset_elim by metis
  qed
  qed
qed

lemma mult_eq_is_mul_eq: assumes "trans r" shows "mult_eq r = mul_eq r" proof
 show "mult_eq r  mul_eq r" proof
  fix N M assume A: "(N,M)  mult_eq r" show "(N,M)  mul_eq r" proof (cases "(N,M)  mult r")
   case True thus ?thesis unfolding mult_is_mul[OF assms] mul_def mul_eq_def by auto
  next
   case False hence eq: "N = M" using A rtranclD unfolding mult_def mult_eq_def by metis
   hence "M = M + {#}  N = N + {#}  set_mset {#}  dm r {#}" by auto
   thus ?thesis unfolding eq unfolding mul_eq_def by fast
  qed
 qed
 show "mul_eq r  mult_eq r" using one_step_implies_mult_eq[OF assms] unfolding mul_eq_def by auto
qed

lemma "mul_eq r = (mul r)=" proof
 show "mul_eq r  (mul r)=" proof
  fix M N assume A:"(M,N)  mul_eq r" show "(M,N)  (mul r)=" proof -
   from A obtain I J K where 1: "M = I + K" and 2: "N = I + J" and 3: "set_mset K  dm r J" unfolding mul_eq_def by auto
   show ?thesis proof (cases "J = {#}")
    case True hence "K = {#}" using 3 unfolding dm_def ds_def by auto
    hence "M = N" using True 1 2 by auto
    thus ?thesis by auto
   next
    case False thus ?thesis using 1 2 3 unfolding mul_def mul_eq_def by auto
   qed
  qed
 qed
 show "mul_eq r  (mul r)=" proof
  fix M N assume A:"(M,N)  (mul r)=" show "(M,N)  mul_eq r"
   proof (cases "M = N")
    case True hence "M = M + {#}" and "N = M + {#}" and "set_mset {#}  dm r {#}" by auto
    thus ?thesis unfolding mul_eq_def by fast
   next
    case False hence "(M,N)  mul r" using A by auto
    thus ?thesis unfolding mul_def mul_eq_def by auto
  qed
 qed
qed

textuseful properties on multisets
lemma mul_eq_reflexive: "(M,M)  mul_eq r" proof -
 have "M = M + {#}" and "set_mset {#}  dm r {#}" by auto
 thus ?thesis unfolding mul_eq_def by fast
qed

lemma mul_eq_trans: assumes "trans r" and "(M,N)  mul_eq r" and "(N,P)  mul_eq r" shows "(M,P)  mul_eq r"
 using assms unfolding mult_eq_is_mul_eq[symmetric,OF assms(1)] mult_eq_def
by auto

lemma mul_eq_singleton: assumes "(M, {#α#})  mul_eq r" shows "M = {#α#}  set_mset M  dm r {#α#}" proof -
 from assms obtain I J K where 1:"M = I + K" and 2:"{#α#} = I + J" and 3:"set_mset K  dm r J" unfolding mul_eq_def by auto
 thus ?thesis proof (cases "I = {#}")
  case True hence "J = {#α#}" using 2 by auto
  thus ?thesis using 1 3 True by auto
 next
  case False hence i: "I = {#α#}" using 2 union_is_single by metis
  hence "J = {#}" using 2 union_is_single by metis
  thus ?thesis using 1 i 3 unfolding dm_def ds_def by auto
 qed
qed

lemma mul_and_mul_eq_imp_mul: assumes "trans r" and "(M,N)  mul r" and "(N,P)  mul_eq r" shows "(M,P)  mul r"
 using assms unfolding mult_is_mul[symmetric,OF assms(1)] mult_eq_is_mul_eq[symmetric,OF assms(1)] mult_def mult_eq_def by auto

lemma mul_eq_and_mul_imp_mul: assumes "trans r" and "(M,N)  mul_eq r" and "(N,P)  mul r" shows "(M,P)  mul r"
 using assms unfolding mult_is_mul[symmetric,OF assms(1)] mult_eq_is_mul_eq[symmetric,OF assms(1)] mult_def mult_eq_def by auto

lemma wf_mul: assumes "trans r" and "wf r" shows "wf (mul r)"
 unfolding mult_is_mul[symmetric,OF assms(1)] using wf_mult[OF assms(2)] by auto

lemma remove_is_empty_imp_mul: assumes "M -s dm r {#α#} = {#}" shows "(M,{#α#})  mul r" proof -
 from assms have C: "set_mset M  dm r {#α#}" by (metis remove_empty_implies_subset)
 have "M = {#}+M" and "{#α#}={#}+{#α#}" and "{#α#}  {#}" by auto
 thus ?thesis using C unfolding mul_def by fast
qed

text Lemma 2.6

lemma lemma2_6_1_set: "ds r (S  T) = ds r S  ds r T"
 unfolding set_mset_union ds_def by auto

lemma lemma2_6_1_list: "dl r (σ@τ) = dl r σ  dl r τ"
 unfolding dl_def ds_def set_append by auto

lemma lemma2_6_1_multiset: "dm r (M + N) = dm r M  dm r N"
 unfolding dm_def set_mset_union ds_def by auto

lemma lemma2_6_1_diff: "(dm r M) - ds r S  dm r (M -s S)"
 unfolding diff_def dm_def ds_def by (rule subsetI) auto

text missing but useful
lemma dl_monotone: "dl r (σ@τ)  dl r (σ@τ'@τ)" unfolding lemma2_6_1_list by auto

text Lemma 2.6.2

lemma lemma2_6_2_a: assumes t: "trans r" and "M ⊆# N" shows "(M,N)  mul_eq r" proof -
 from assms(2) obtain J where "N=M+J" by (metis assms(2) mset_subset_eq_exists_conv)
 hence "M = M + {#}" and "N = M + J" and "set_mset {#}  dm r J" by auto
 thus ?thesis unfolding mul_eq_def by fast
qed

lemma mul_eq_not_equal_imp_elt:
assumes "(M,N)mul_eq r" and "yset_mset M - set_mset N" shows "zset_mset N.(y,z)r" proof -
 from assms obtain I J K where "N=I+J" and "M=I+K" and F3:"set_mset K  dm r J" unfolding mul_eq_def by auto
 thus ?thesis using assms(2) downset_elim[OF F3] by auto
qed

lemma lemma2_6_2_b: assumes "trans r" and "(M,N)  mul_eq r" shows "dm r M  dm r N" proof
 fix x assume A: "x  dm r M" show "x  dm r N" proof -
  from A obtain y where F2:"yset_mset M" and F3:"(x,y)r" unfolding dm_def ds_def by auto
  hence " z  set_mset N. (x,z)r" proof (cases "yset_mset N")
   case True thus ?thesis using F3 unfolding ds_def by auto
   next
   case False thus ?thesis using mul_eq_not_equal_imp_elt assms F2 F3 trans_def by fast
  qed
  thus ?thesis unfolding dm_def ds_def by auto
 qed
qed

text Lemma 2.6.3
lemma ds_trans_contrapos: assumes t: "trans r" and "x  ds r S" and "(x,y)  r" shows "y  ds r S"
 using assms unfolding ds_def trans_def by fast

lemma dm_max_elt: assumes i: "irrefl r" and t: "trans r"  shows "x  dm r M   y  set_mset (M -s dm r M). (x,y)  r"
 proof (induct M arbitrary: x)
  case empty thus ?case unfolding dm_def ds_def by auto
 next
  case (add p P)
  hence mem: "x  (dm r P  dm r {#p#})" unfolding dm_def ds_def by auto
  from i t have not_mem_dm: "p  dm r {#p#}" unfolding dm_def ds_def irrefl_def by auto
  thus ?case
  proof (cases "x  dm r P")
   case False hence relp: "(x,p)  r" using mem unfolding dm_def ds_def by auto
   show ?thesis proof (cases "p  dm r P")
    case True thus ?thesis using relp t ds_trans_contrapos False unfolding dm_def by fast
     next
    case False thus ?thesis using not_mem_dm relp unfolding dm_def ds_def diff_def by auto
   qed
  next
    case True obtain y where key: "y  set_mset P" "y  dm r P" "(x,y)  r" using add(1)[OF True] unfolding diff_def by auto
    thus ?thesis
    proof (cases "y  dm r {#p#}")
     case True hence rely: "(y,p)  r" unfolding dm_def ds_def by auto
     hence relp: "(x,p)  r" using rely t key trans_def by metis
     have not_memp: "p  set_mset P" using rely key unfolding dm_def ds_def by auto
     have memp: "p  set_mset (P + {#p#})" by auto
     have "p  dm r P" using ds_trans_contrapos[OF t] key(2) rely unfolding dm_def by auto
     hence "p  dm r (P + {#p#})" using not_mem_dm unfolding dm_def ds_def by auto
     thus ?thesis using relp unfolding diff_def by auto
    next
     case False thus ?thesis using key unfolding dm_def ds_def diff_def by auto
    qed
  qed
 qed

lemma dm_subset: assumes i:"irrefl r" and t: "trans r"  shows "dm r M  dm r (M -s dm r M)"
 using assms dm_max_elt unfolding dm_def ds_def by fast

lemma dm_eq: assumes i:"irrefl r" and t: "trans r" shows "dm r M = dm r (M -s dm r M)"
 using dm_subset[OF assms] unfolding dm_def ds_def diff_def by auto

lemma lemma2_6_3: assumes t:"trans r" and i:"irrefl r" and "(M,N)  mul_eq r"
 shows " I' J' K' . N = I' + J'  M = I' + K'  J' ∩# K' = {#}  set_mset K'  dm r J'"
proof -
 from assms obtain I J K where 1:"N = I + J" and 2:"M = I + K"  and 3:"set_mset K  dm r J" unfolding mul_eq_def by auto
 have "set_mset (J ∩# K)  r ↓m J" using 3 by auto
 then obtain A where "r ↓m J = set_mset (J ∩# K)  A"
  by blast
 then have key: "set_mset (J -s dm r J)  set_mset (J - (J ∩# K))"
  by clarsimp (metis Multiset.count_diff add.left_neutral add_diff_cancel_left' mem_Collect_eq not_gr0 set_mset_def)
 from 1 2 3 have "N = (I + (J ∩# K)) + (J - (J ∩# K))"
  by (metis diff_union_cancelL subset_mset.inf_le2 multiset_diff_union_assoc multiset_inter_commute union_commute union_lcomm)
 moreover have "M = (I + (J ∩# K)) + (K - (J ∩# K))"
  by (rule multiset_eqI) (simp add: 2)
 moreover have "set_mset (K-(J∩#K))  dm r (J-(J∩#K))"
 proof -
  have "set_mset (K-(J∩#K))  dm r J" using 3
    by (meson Multiset.diff_subset_eq_self mset_subset_eqD subset_eq)
  moreover have "... = dm r (J -s dm r J)" using dm_eq[OF i t] by auto
  moreover have "...  dm r (J - (J ∩# K))" using ds_monotone[OF key] unfolding dm_def by auto
  ultimately show ?thesis by auto
qed
 moreover have "(J-(J∩#K)) ∩# (K-(J∩#K)) = {#}" by (rule multiset_eqI) auto
 ultimately show ?thesis by auto
qed

(*  (* initial proof by Bertram Felgenhauer *)
lemma lemma2_6_3_step:
assumes t:"trans r" and i:"irrefl r" and P:"set_mset K ⊆ dm r J" shows "set_mset (K-(J∩#K)) ⊆ dm r (J-(J∩#K))" proof
 fix k assume K: "k ∈ set_mset (K - (J∩#K))" show "k ∈ dm r (J - (J∩#K))" proof -
  have k: "k ∈# K" using K by simp
  have step: "k ∈ dm r (J-K)" proof -
   {
   fix P have "P ≤ K ⟹ k ∈ dm r (J-P)" using k proof (induct P arbitrary:k rule:multiset_induct)
    case empty thus ?case using P by auto
   next
    case (add Q q)
    have h1: "q ∈# K" and h2: "Q ≤ K" using mset_subset_eq_insertD[OF add(2)] by auto
    obtain j where mem1: "j∈set_mset (J - Q)" and rel1: "(k, j) ∈ r" using add(1)[OF h2 add(3)] unfolding dm_def ds_def by auto
    show ?case proof (cases "j ∈# J - (Q + {#q#})")
     case True thus ?thesis using rel1 unfolding dm_def ds_def by force
    next
     case False hence eq: "q = j" using mem1 by (cases "q = j") auto
     obtain j2 where mem2: "j2∈set_mset (J - Q)" and rel2: "(j, j2) ∈ r" using eq add(1)[OF h2 h1] unfolding dm_def ds_def by auto
     have rel: "(k,j2) ∈ r" using transD[OF assms(1) rel1 rel2] by auto
     have "j2 ≠ q" using rel2 eq i irrefl_def by fast
     thus ?thesis using rel mem2 unfolding dm_def ds_def by (cases "j2=k") auto
    qed
   qed
   }
   thus ?thesis by auto
  qed
  have eq: "J - K = J - (J ∩# K)" by (rule multiset_eqI) auto
  show ?thesis using step unfolding eq dm_def ds_def by auto
 qed
qed

lemma lemma2_6_3: assumes t: "trans r" and i: "irrefl r" and "(M,N) ∈ mul_eq r"
shows "∃ I J K. N = I + J ∧ M = I + K ∧ J∩#K = {#} ∧ set_mset K ⊆ dm r J" proof -
 from assms(1,3)
 obtain I J K where f1:"N = I + J" and f2:"M = I + K" and f3:"set_mset K ⊆ dm r J" unfolding mul_eq_def by fast
 hence "N = (I + (J ∩# K)) + (J - (J ∩# K))"
  by (metis diff_union_cancelL inf_le2 multiset_diff_union_assoc multiset_inter_commute union_commute union_lcomm)
 moreover have "M = (I + (J ∩# K)) + (K - (J ∩# K))"
  by (metis diff_le_self diff_union_cancelL f1 f2 f3 multiset_diff_union_assoc multiset_inter_commute multiset_inter_def union_assoc)
 moreover have "(J-(J∩#K)) ∩# (K-(J∩#K)) = {#}" by (rule multiset_eqI) auto
 ultimately show ?thesis using lemma2_6_3_step[OF t i f3] by auto
qed
*)

text Lemma 2.6.4
lemma lemma2_6_4: assumes t: "trans r" and "N  {#}" and "set_mset M  dm r N" shows "(M,N)  mul r" proof -
 have "M = {#} + M" and "N = {#} + N" using assms by auto
 thus ?thesis using assms(2,3) unfolding mul_def by fast
qed

lemma lemma2_6_5_a: assumes t: "trans r" and "ds r S  S" and "(M,N)  mul_eq r"
shows "(M -s S, N -s S)  mul_eq r"
proof -
 from assms(1,3)
 obtain I J K where a: "N=I+J" and b:"M=I+K" and c:"set_mset K  dm r J" unfolding mul_eq_def by best
 from a b have "M -s S = I -s S + K -s S"
   "N -s S = I -s S + J -s S" by (auto simp add: lemmaA_3_8)
 moreover have "set_mset (K-sS)  dm r (J-sS)" proof -
  have "set_mset (K-sS)  set_mset (K-s (ds r S))" using assms(2) unfolding diff_def by auto
  moreover have "set_mset(K-s (ds r S))  (dm r J) - (ds r S)" using c unfolding diff_def by auto
  moreover have "(dm r J) - (ds r S)  dm r (J -s S)" using lemma2_6_1_diff by fast
  ultimately show ?thesis by auto
 qed
 ultimately show ?thesis by (rule in_mul_eqI)
qed

lemma lemma2_6_5_a': assumes t:"trans r" and "(M,N)  mul_eq r" shows "(M -s ds r S, N -s ds r S)  mul_eq r"
  using assms lemma2_6_5_a[OF t] ds_ds_subseteq_ds[OF t] by auto

text Lemma 2.6.6
lemma lemma2_6_6_a: assumes t: "trans r" and "(M,N)  mul_eq r" shows "(Q + M,Q + N)  mul_eq r" proof -
 obtain I J K where A:"Q+N=(Q+I)+J" and B:"Q+M=(Q+I)+K" and C:"set_mset K  dm r J"
  using assms(2) unfolding mul_eq_def by auto
  thus ?thesis using C unfolding mul_eq_def by blast
qed

lemma add_left_one:
 assumes  " I J K. add_mset q N = I + J  add_mset q  M = I + K  (J∩#K={#})  set_mset K  dm r J"
 shows " I2 J K. N = I2 + J  M = I2 + K  set_mset K  dm r J" proof -
 from assms obtain I J K where A: "{#q#} + N = I + J" and B:"{#q#} + M = I + K"
  and C:"(J ∩# K = {#})" and D:"set_mset K  dm r J" by auto
 have "q∈#I" proof (cases "q ∈# I")
  case True thus ?thesis by auto
 next
  case False
  have "q ∈# J" using False A by (metis UnE multi_member_this set_mset_union) 
  moreover have "q ∈# K" using False B by (metis UnE multi_member_this set_mset_union)
  moreover have "¬ q ∈# (J ∩# K)" using C by auto
  ultimately show ?thesis by auto
 qed
 hence " I2. I = add_mset q I2" by (metis multi_member_split)
 hence " I2. add_mset q N = (add_mset q I2) + J  add_mset q M = (add_mset q I2) + K" using A B by auto
 thus ?thesis using D by auto
qed

lemma lemma2_6_6_b_one :
assumes "trans r" and "irrefl r" and "(add_mset q M, add_mset q N)  mul_eq r" shows "(M,N)  mul_eq r"
 using add_left_one[OF lemma2_6_3[OF assms]] unfolding mul_eq_def by auto

lemma lemma2_6_6_b' : assumes "trans r" and i: "irrefl r" and "(Q + M, Q + N)  mul_eq r"
 shows "(M,N)  mul_eq r" using assms(3) proof (induct Q arbitrary: M N)
 case empty thus ?case by auto
 next
 case (add q Q) thus ?case unfolding union_assoc using lemma2_6_6_b_one[OF assms(1,2)]
   by (metis union_mset_add_mset_left)
 qed

lemma lemma2_6_9: assumes t: "trans r" and "(M,N)  mul r" shows "(Q+M,Q+N)  mul r" proof -
 obtain I J K where F1:"N = I + J" and F2:"M = I + K"and F3:"set_mset K  dm r J" and F4:"J  {#}"
  using assms unfolding mul_def by auto
 have "Q+N=Q+I+J" and "Q+M=Q+I+K" by (auto simp: F1 F2 union_commute union_lcomm)
  thus ?thesis using assms(1) F3 F4 unfolding mul_def by blast
qed

text Lemma 2.6.7
lemma lemma2_6_7_a: assumes t: "trans r" and "set_mset Q  dm r N - dm r M" and "(M,N)  mul_eq r"
shows "(Q+M,N)  mul_eq r" proof -
 obtain I J K where A: "N=I+J" and B:"M=I+K" and C:"set_mset K  dm r J" using assms unfolding mul_eq_def by auto
 hence "set_mset(Q+K)  dm r J" using assms lemma2_6_1_diff unfolding dm_def ds_def by auto
 hence "(I+(Q+K),I+J)  mul_eq r" unfolding mul_eq_def by fast
 thus ?thesis using A B C union_assoc union_commute by metis
qed

text missing?; similar to lemma\_2.6.2?
lemma lemma2_6_8: assumes t: "trans r" and "S  T" shows "(M -s T,M -s S)  mul_eq r" proof -
 from assms(2) have "(M -s T) ⊆# (M -s S)"
  by (metis Un_absorb2 Un_commute lemmaA_3_10 lemmaA_3_9 mset_subset_eq_add_right)
 thus ?thesis using lemma2_6_2_a[OF t] by auto
qed

subsubsection Lexicographic maximum measure
text Def 3.1: lexicographic maximum measure
fun lexmax :: "'a rel  'a list  'a multiset" where
   "lexmax r [] = {#}"
 | "lexmax r (α#σ) =  {#α#} + (lexmax r σ -s ds r {α})"

notation
 lexmax ("_|_|" [1000] 1000)

lemma lexmax_singleton: "r|[α]| = {#α#}" unfolding lexmax.simps diff_def by simp

text Lemma 3.2

text Lemma 3.2(1)
lemma lemma3_2_1: assumes t: "trans r" shows "r ↓m r|σ| = r ↓l σ" proof (induct σ)
 case Nil show ?case unfolding dm_def dl_def by auto
 next
 case (Cons α σ)
 have "dm r {#α#}  dm r (r|σ| -s ds r {α}) = dm r {#α#}  dl r σ" (is "?L = ?R") proof -
  have "?L  ?R" unfolding Cons[symmetric] diff_def dm_def ds_def by auto
  moreover have "?R  ?L" proof
   fix x assume A: "x  ?R" show "x  ?L" proof (cases "x  dm r {#α#}")
    case True thus ?thesis by auto
   next
    case False
    hence mem: "x  dm r (lexmax r σ)" using A Cons by auto
    have "x  (ds r (ds r {α}))" using False ds_ds_subseteq_ds[OF t] unfolding dm_def by auto
    thus ?thesis using mem lemma2_6_1_diff by fast
   qed
  qed
  ultimately show ?thesis by auto
 qed
 thus ?case unfolding lemma2_6_1_multiset lexmax.simps dl_def dm_def ds_def by auto
qed

text Lemma 3.2(2)
lemma lemma3_2_2: "r|σ@τ| = r|σ| + (r|τ| -s r ↓l σ)" proof(induct σ)
 case Nil thus ?case unfolding dl_def ds_def lexmax.simps apply auto unfolding diff_empty by auto
 next
 case (Cons α σ)
  have "lexmax r (α#σ@τ) = {#α#} + ((lexmax r (σ@τ)) -s (ds r {α}))" by auto
  moreover have " = {#α#} + ((lexmax r σ + ((lexmax r τ) -s (dl r σ))) -s (ds r {α}))"
   using Cons by auto
  moreover have " = {#α#} + ((lexmax r σ) -s (ds r {α})) + (((lexmax r τ) -s (dl r σ)) -s (ds r {α}))"
   unfolding lemmaA_3_8 unfolding union_assoc by auto
  moreover have " = lexmax r (α#σ) + (((lexmax r τ) -s (dl r σ)) -s (ds r {α}))" by simp
  moreover have " = lexmax r (α#σ) + ((lexmax r τ) -s (dl r (α#σ)))" unfolding lemmaA_3_9 dl_def dm_def lemma2_6_1_set[symmetric] by auto
  ultimately show ?case unfolding diff_def by simp
qed

text Definition 3.3

definition D :: "'a rel  'a list  'a list  'a list  'a list  bool" where
 "D r τ σ σ' τ' = ((r|σ@τ'|, r|τ| + r|σ| )  mul_eq r
                  (r|τ@σ'|, r|τ| + r|σ| )  mul_eq r)"

lemma D_eq: assumes "trans r" and "irrefl r" and "D r τ σ σ' τ'"
 shows "(r|τ'| -s dl r σ,r|τ| )  mul_eq r" and "(r|σ'| -s dl r τ,r|σ| )  mul_eq r"
 using assms unfolding D_def lemma3_2_2 using union_commute lemma2_6_6_b' apply metis
 using assms unfolding D_def lemma3_2_2 using union_commute lemma2_6_6_b' by metis

lemma D_inv: assumes "trans r" and "irrefl r" and "(r|τ'| -s dl r σ,r|τ| )  mul_eq r"
                                                and "(r|σ'| -s dl r τ,r|σ| )  mul_eq r"
 shows "D r τ σ σ' τ'"
 using assms unfolding D_def lemma3_2_2 using lemma2_6_6_a[OF assms(1)] union_commute by metis

lemma D: assumes "trans r" and "irrefl r"
 shows  "D r τ σ σ' τ' = ((r|τ'| -s dl r σ,r|τ| )  mul_eq r
                         (r|σ'| -s dl r τ,r|σ| )  mul_eq r)"
 using assms D_eq D_inv by auto

lemma mirror_D: assumes "trans r" and "irrefl r" and "D r τ σ σ' τ'" shows "D r σ τ τ' σ'"
 using assms D by metis

text Proposition 3.4

definition LD_1' :: "'a rel  'a  'a  'a list  'a list  'a list  bool"
 where "LD_1' r β α σ1 σ2 σ3 =
 (set σ1  ds r {β}  length σ2  1  set σ2  {α}  set σ3  ds r {α,β})"

definition LD' :: "'a rel  'a  'a
   'a list  'a list  'a list  'a list  'a list  'a list  bool"
 where "LD' r β α σ1 σ2 σ3 τ1 τ2 τ3 = (LD_1' r β α σ1 σ2 σ3  LD_1' r α β τ1 τ2 τ3)"

text auxiliary properties on multisets

lemma lexmax_le_multiset: assumes t:"trans r" shows "r|σ| ⊆# mset σ" proof (induct "σ")
 case Nil thus ?case unfolding lexmax.simps by auto
 next
 case (Cons s τ) hence "lexmax r τ -s ds r {s} ⊆# mset τ" using lemmaA_3_10 mset_subset_eq_add_right subset_mset.order_trans by metis
 thus ?case by simp
qed

lemma split: assumes "LD_1' r β α σ1 σ2 σ3" shows "σ2 = []  σ2 = [α]"
 using assms unfolding  LD_1'_def by (cases σ2) auto

lemma proposition3_4_step: assumes "trans r" and "irrefl r" and "LD_1' r β α σ1 σ2 σ3"
shows "(r|σ1@σ2@σ3| -s (dm r {#β#}), r|[α]| )  mul_eq r" proof -
 from assms have "set σ1  dm r {#β#}" unfolding LD'_def LD_1'_def dm_def by auto
 hence "set_mset (lexmax r σ1)  dm r {#β#}" using submultiset_implies_subset[OF lexmax_le_multiset[OF assms(1)]] by auto
 hence one: "lexmax r σ1 -s dm r {#β#} = {#}" using subset_implies_remove_empty by auto
 from assms have "set σ3  dl r σ2  dl r σ1  dm r {#β#}  dm r {#α#}" (is "?l  ?r") unfolding LD'_def LD_1'_def dm_def ds_def by auto
 hence "set_mset (lexmax r σ3)  ?r " using submultiset_implies_subset[OF lexmax_le_multiset[OF assms(1)]] by auto
 hence pre3: "lexmax r σ3 -s ?r = {#}" using subset_implies_remove_empty by auto
 show ?thesis proof (cases "σ2 = []")
  case True
  hence two:"(lexmax r σ2 -s dl r σ1) -s dm r {#β#} = {#}" unfolding diff_def by auto
  from pre3 have "(((lexmax r σ3 -s dl r σ2) -s dl r σ1) -s dm r {#β#}) -s dm r {#α#} = {#}" unfolding True dl_def lemmaA_3_9 by auto
  hence three:"(((lexmax r σ3 -s dl r σ2) -s dl r σ1) -s dm r {#β#},{#α#})  mul r" using remove_is_empty_imp_mul by metis
  show ?thesis using three unfolding lemma3_2_2 lexmax_singleton lemmaA_3_8 one two mul_def mul_eq_def by auto
 next
  case False hence eq: "σ2 = [α]" using split[OF assms(3)] by fast
  have two: "((lexmax r σ2 -s dl r σ1) -s dm r {#β#},{#α#})  mul_eq r" using lemma2_6_8[OF assms(1) empty_subsetI] unfolding eq lexmax.simps diff_from_empty lemmaA_3_9 diff_empty by auto
  from pre3 have "lexmax r σ3 -s ((dl r σ2  dm r {#α#})  dl r σ1  dm r {#β#}) = {#}" unfolding eq lemmaA_3_9 using Un_assoc Un_commute by metis
  hence three: "((lexmax r σ3 -s dl r σ2) -s dl r σ1) -s dm r {#β#} = {#}" using Un_absorb unfolding lemmaA_3_9 eq dm_def dl_def by auto
  show ?thesis unfolding lemma3_2_2 lexmax_singleton lemmaA_3_8 one three using two by auto
 qed
qed

lemma proposition3_4:
assumes t: "trans r" and i: "irrefl r" and ld: "LD' r β α σ1 σ2 σ3 τ1 τ2 τ3"
shows "D r [β] [α] (σ1@σ2@σ3) (τ1@τ2@τ3)"
 using proposition3_4_step[OF t i] ld unfolding LD'_def D[OF assms(1,2)] dl_def dm_def by auto

(*reverse direction*)

lemma lexmax_decompose: assumes "α ∈# r|σ|" shows "σ1 σ3. (σ=σ1@[α]@σ3  α  dl r σ1)"
using assms proof (induct σ)
 case Nil thus ?case by auto
 next
 case (Cons β as) thus ?case proof (cases "α=β")
  case True
  from this obtain σ1 σ3 where dec: "β#as = σ1@[α]@σ3" and empty: "σ1 = []" by auto
  hence "α  dl r σ1" unfolding dl_def ds_def by auto
  thus ?thesis using dec by auto
 next
  case False hence "α ∈# r|as|-s ds r {β}" using Cons(2) by auto
  hence x: "α ∈# r|as|  α  ds r {β}"
    by simp
  from this obtain σ1 σ3 where "as = σ1 @ [α] @ σ3" and w: "α  dl r σ1" using Cons(1) by auto
  hence  "β#as = (β#σ1) @ [α] @ σ3" and  "α  dl r (β#σ1)" using x w unfolding dm_def dl_def ds_def by auto
  thus ?thesis by fast
 qed
qed

lemma lexmax_elt: assumes "trans r" and "x  (set σ)" and "x  set_mset r|σ|"
shows "y. (x,y)  r  y  set_mset r|σ|"  using assms(2,3) proof (induct σ)
 case Nil thus ?case by auto
next
 case (Cons a as) thus ?case proof (cases "x  set_mset r|as|")
   case True
   from Cons True obtain y where s: "(x, y)  r  y  set_mset r|as|" by auto
   thus ?thesis proof (cases "y  ds r {a}")
    case True thus ?thesis using transD[OF assms(1)] s unfolding dm_def ds_def by auto
   next
    case False thus ?thesis using s unfolding lexmax.simps diff_def by auto
   qed
  next
   case False thus ?thesis using Cons unfolding diff_def dm_def ds_def lexmax.simps by auto
  qed
 qed

lemma lexmax_set: assumes "trans r" and "set_mset r|σ|  r ↓s S" shows "set σ  r ↓s S" proof
 fix x assume A: "x  set σ" show "x  ds r S" proof (cases "x  set_mset r|σ|")
  case True thus ?thesis using assms by auto
 next
  case False from lexmax_elt[OF assms(1) A False] obtain y
  where rel: "(x,y)  r  y  set_mset r|σ|" by auto
  hence "y  ds r S" using assms by auto
  thus ?thesis using rel assms transD unfolding dm_def ds_def by fast
 qed
qed

lemma drop_left_mult_eq:
assumes "trans r" and "irrefl r" and "(N+M,M)  mul_eq r" shows "N = {#}" proof -
 have "(M+N,M+{#})  mul_eq r" using assms(3) apply auto using union_commute by metis
 hence k:"(N,{#})  mul_eq r" using lemma2_6_6_b'[OF assms(1,2)] by fast
 from this obtain I J K where "{#} = I + J  N = I + K  set_mset K  dm r J" unfolding mul_eq_def by fast
 thus ?thesis unfolding dm_def ds_def by auto
qed

text generalized to lists
lemma proposition3_4_inv_lists:
assumes t: "trans r" and i: "irrefl r" and k:"(r|σ| -s r ↓l β, {#α#})  mul_eq r" (is "(?M,_)  _")
shows " σ1 σ2 σ3. ((σ = σ1@σ2@σ3)  set σ1  dl r β  length σ2  1  set σ2  {α})  set σ3  dl r (α#β)"  proof (cases "α ∈# ?M")
  case True hence "α ∈# r|σ|" by simp
  from this obtain σ1 σ3 where sigma: "σ=σ1@[α]@σ3" and alpha: "α  dl r σ1" using lexmax_decompose by metis
  hence dec: "((r|σ1|-sdl r β) + (r|[α]|-s (dl r σ1  dl r β)) + (r|σ3| -s (dl r [α]  dl r σ1  dl r β)), {#α#})  mul_eq r" (is "(?M1 + ?M2 + ?M3,_)  _")
   using k unfolding sigma lemma3_2_2 lemmaA_3_8 lemmaA_3_9 LD_1'_def union_assoc by auto

  from True have key: "α  dl r β" by simp
  hence "?M2 = {#α#}" unfolding lexmax_singleton diff_def using alpha by auto
  hence "(?M1+?M3 + {#α#},{#α#})  mul_eq r" using dec union_assoc union_commute by metis
  hence w: "?M1+?M3 = {#}" using drop_left_mult_eq assms(1,2) by blast
  from w have "(r|σ1|-sdl r β) = {#}" by auto
  hence "set_mset r|σ1|  ds r (set β)" using remove_empty_implies_subset unfolding dl_def dm_def by auto
  hence sigma1: "set σ1  ds r (set β)" using lexmax_set[OF assms(1)] by auto

  have sigma2: "length [α]  1  set [α]  {α}" by auto

  have sub:"dl r σ1  dl r β" using subset_imp_ds_subset[OF assms(1) sigma1] unfolding dm_def dl_def by auto
  hence sub2: "dl r σ1  dl r β = dl r β" by auto
  from w have  "?M3 = {#}" by auto
  hence "r|σ3|-s (ds r {α}  ds r (set β)) = {#}" unfolding Un_assoc sub2 unfolding dl_def by auto
  hence "r|σ3|-s (ds r ({α}  (set β))) = {#}" unfolding lemma2_6_1_set[symmetric] by metis
  hence "set_mset r|σ3|  ds r ({α}  (set β))" using remove_empty_implies_subset by auto
  hence sigma3: "set σ3  ds r ({α}  (set β))" using lexmax_set[OF assms(1)] by auto
  show ?thesis using sigma sigma1 sigma2 sigma3 unfolding dl_def apply auto by (metis One_nat_def append_Cons append_Nil sigma2)
 next
  case False hence "set_mset ?M  dm r {#α#}" using mul_eq_singleton[OF k]
    by (auto dest: diff_eq_singleton_imp)
  hence "set_mset r|σ|  ds r ({α}  (set β))" unfolding diff_def dm_def dl_def ds_def by auto
  hence "set σ  ds r ({α}  (set β))" using lexmax_set[OF assms(1)] by auto
  thus ?thesis unfolding dl_def apply auto by (metis append_Nil bot_least empty_set le0 length_0_conv)
 qed

lemma proposition3_4_inv_step:
assumes t: "trans r" and i: "irrefl r" and k:"(r|σ| -s r ↓l [β], {#α#})  mul_eq r" (is "(?M,_)  _")
shows " σ1 σ2 σ3. ((σ = σ1@σ2@σ3)  LD_1' r β α σ1 σ2 σ3)"
 using proposition3_4_inv_lists[OF assms] unfolding LD_1'_def dl_def by auto

lemma proposition3_4_inv:
assumes t: "trans r" and i: "irrefl r" and "D r [β] [α] σ τ"
shows " σ1 σ2 σ3 τ1 τ2 τ3. (σ = σ1@σ2@σ3  τ = τ1@τ2@τ3  LD' r β α σ1 σ2 σ3 τ1 τ2 τ3)"
using proposition3_4_inv_step[OF assms(1,2)] D_eq[OF assms] unfolding lexmax_singleton LD'_def by metis

text Lemma 3.5
lemma lemma3_5_1:
assumes t: "trans r" and "irrefl r" and "D r τ σ σ' τ'" and "D r υ σ' σ'' υ'"
shows "(lexmax r (τ @ υ @ σ''), lexmax r (τ @ υ) + lexmax r σ)  mul_eq r" proof -
 have "lexmax r (τ @ υ @ σ'') = (lexmax r (τ @ υ) + ((lexmax r σ'') -s (dl r (τ@υ))))"
  unfolding append_assoc[symmetric] using lemma3_2_2 by fast
 moreover have x:" = lexmax r (τ@υ) + (((lexmax r σ'') -s dl r υ) -s dl r τ)"
  by (auto simp: lemma2_6_1_list lemmaA_3_9 Un_commute)
 moreover have "(,lexmax r (τ@υ) + (lexmax r σ' -s dl r τ))  mul_eq r" (is "(_,?R)  _")
  using lemma2_6_6_a[OF t lemma2_6_5_a'[OF t D_eq(2)[OF assms(1,2,4)]]] unfolding dl_def by auto
 moreover have "(?R,lexmax r (τ@υ) + lexmax r σ)  mul_eq r"
  using lemma2_6_6_a[OF t D_eq(2)[OF assms(1-3)]] by auto
 ultimately show ?thesis using mul_eq_trans[OF t] by metis
 qed

lemma claim1: assumes t: "trans r" and "D r τ σ σ' τ'"
shows "(r|σ@τ'| + ((r|υ'| -s r ↓l (σ@τ')) ∩s r ↓l τ),r|σ| + r|τ| )  mul_eq r" (is "(?F+?H,?G)  _")
proof -
 have 1: "(?F,?G)  mul_eq r" using assms(2) unfolding D_def by (auto simp: union_commute)
 have 2: "set_mset ?H  (dm r ?G) - (dm r ?F)" (is "(?L  _)") proof -
  have "set_mset ?H = set_mset ((lexmax r υ' ∩s dl r τ) -s dl r (σ@τ'))" unfolding lemmaA_3_11 by auto
  moreover have  "  (dl r τ - dl r (σ@τ'))" unfolding diff_def intersect_def by auto
  moreover have "...  ((dl r σ  dl r τ) - dl r (σ@τ'))" by auto
  ultimately show ?thesis unfolding lemma2_6_1_multiset lemma3_2_1[OF t] by auto
 qed
show ?thesis using lemma2_6_7_a[OF t 2 1] by (auto simp: union_commute)
qed

lemma step3: assumes t:"trans r" and "D r τ σ σ' τ'"
shows "r ↓l (σ@τ)  (r ↓m (r|σ'| + r|τ| ))" proof -
 have a: "dl r (σ@τ) = dm r (lexmax r τ + lexmax r σ)" and b: "dl r (τ@σ') = dm r (lexmax r σ' + lexmax r τ)"
   unfolding lemma2_6_1_list lemma3_2_1[OF t,symmetric] lemma2_6_1_multiset by auto
 show ?thesis using assms(2) lemma2_6_2_b[OF t] lemma3_2_1[OF t,symmetric] unfolding D_def a b[symmetric] by auto
qed

lemma claim2: assumes t: "trans r" and "D r τ σ σ' τ'"
shows "((r|υ'| -s  r ↓l (σ@τ')) -s r ↓l τ, (r|υ'| -s r ↓l σ') -s r ↓l τ)  mul_eq r" (is "(?L,?R)  _")
 proof -
  have "?L = lexmax r υ' -s (dl r (σ@τ'@τ))" unfolding lemmaA_3_9 append_assoc[symmetric] lemma2_6_1_list by auto
  moreover have "(,lexmax r υ' -s dl r (σ@τ))  mul_eq r" (is "(_,?R)  _") using lemma2_6_8[OF t dl_monotone] by auto
  moreover have  "(?R,lexmax r υ' -s dm r (lexmax r σ' + lexmax r τ))  mul_eq r" (is "(_,?R)  _") using lemma2_6_8[OF t step3[OF assms]] by auto
  moreover have "?R = (lexmax r υ' -s dl r σ') -s dl r τ" unfolding lemma3_2_1[OF t,symmetric] lemma2_6_1_multiset lemmaA_3_9[symmetric] by auto
  ultimately show ?thesis using mul_eq_trans[OF t] by metis
 qed

lemma lemma3_5_2: assumes "trans r" and "irrefl r" and "D r τ σ σ' τ'" and "D r υ σ' σ'' υ'"
 shows "(r|(σ @ τ' @ υ')|, r|σ| + r|(τ@υ)| )  mul_eq r"
proof -
 have 0: "lexmax r (σ@τ'@υ') = lexmax r (σ@τ') + (lexmax r υ' -s dl r (σ@τ'))" (is "?L = _")
  unfolding append_assoc[symmetric] lemma3_2_2 by auto
 moreover have " = lexmax r (σ@τ') + ((lexmax r υ' -s dl r (σ@τ')) ∩s dl r τ) + ((lexmax r υ' -s dl r (σ@τ')) -s dl r τ)"
  using lemmaA_3_10 unfolding union_assoc by auto
 moreover have "(, lexmax r σ + lexmax r τ + ((lexmax r υ' -s dl r (σ@τ')) -s dl r τ))  mul_eq r" (is "(_,?R)  _")
  using assms claim1 lemma2_6_6_a union_commute by metis
 moreover have "(?R, lexmax r σ + lexmax r τ + (((lexmax r υ' -s dl r σ') -s dl r τ)))  mul_eq r" (is "(_,?R)  _")
  using lemma2_6_6_a[OF assms(1) claim2[OF assms(1,3)]] by auto
 moreover have "(?R, lexmax r σ + lexmax r τ + lexmax r υ -s dl r τ)  mul_eq r" (is "(_,?R)  _")
  using lemma2_6_6_a[OF assms(1) lemma2_6_5_a'[OF assms(1) D_eq(1)[OF assms(1,2,4)]]] unfolding dl_def by auto
 moreover have "?R = lexmax r σ + lexmax r (τ@υ)" unfolding union_assoc lemma3_2_2 by auto
 ultimately show ?thesis using mul_eq_trans[OF assms(1)] by metis
qed

lemma lemma3_5: assumes "trans r" and "irrefl r" and "D r τ σ σ' τ'" and "D r υ σ' σ'' υ'"
shows "D r (τ@υ) σ σ'' (τ'@υ')"
 unfolding D_def append_assoc using assms lemma3_5_1 lemma3_5_2 union_commute by metis

lemma step2: assumes "trans r" and "τ  []" shows "(M ∩s dl r τ,lexmax r τ)  mul r" proof -
 from assms obtain x xs where "τ=x#xs" using list.exhaust by auto
 hence x: "lexmax r τ  {#}" by auto
 from assms(2) have y: "set_mset (M ∩sdl r τ)  dm r (lexmax r τ)" unfolding lemma3_2_1[OF assms(1)] intersect_def by auto
 show ?thesis using lemma2_6_4[OF assms(1) x y] by auto
qed

text Lemma 3.6
lemma lemma3_6: assumes t: "trans r" and ne: "τ  []" and D: "D r τ σ σ' τ'"
shows "(r|σ'| + r|υ|, r|σ| + r|τ@υ| )  mul r" (is "(?L,?R)  _") proof -
 have "?L = ((lexmax r σ' + lexmax r υ) ∩s dl r τ) + ((lexmax r σ' + lexmax r υ) -s dl r τ)"
  unfolding lemmaA_3_10[symmetric] by auto
 moreover have "(,lexmax r τ + ((lexmax r σ' + lexmax r υ) -s dl r τ))  mul r" (is "(_,?R2)  _")
  using lemma2_6_9[OF t step2[OF t ne]] union_commute by metis
 moreover have "?R2 = lexmax r τ + (lexmax r σ' -s dl r τ) + (lexmax r υ -s dl r τ)"
  unfolding lemmaA_3_8 union_assoc[symmetric] by auto
 moreover have " = lexmax r (τ@σ') + (lexmax r υ -s dl r τ)" unfolding lemma3_2_2 by auto
 moreover have "(,lexmax r σ + lexmax r τ + (lexmax r υ -s dl r τ))  mul_eq r" (is "(_,?R5)  _")
  using D unfolding D_def using lemma2_6_6_a[OF t] union_commute by metis
 moreover have "?R5 = ?R" unfolding lemma3_2_2 union_assoc by auto
 ultimately show ?thesis using mul_and_mul_eq_imp_mul t by metis
qed

lemma lemma3_6_v: assumes "trans r" and "irrefl r" and "σ  []" and "D r τ σ σ' τ'"
shows "(r|τ'| + r|υ|, r|τ| + r|σ@υ| )  mul r"
 using assms lemma3_6 mirror_D by fast

subsubsection Labeled Rewriting

text Theorem 3.7
type_synonym ('a,'b) lars = "('a×'b×'a) set"
type_synonym ('a,'b) seq = "('a×('b×'a)list)"

inductive_set seq :: "('a,'b) lars  ('a,'b) seq set" for ars
 where "(a,[])  seq ars"
     | "(a,α,b)  ars  (b,ss)  seq ars  (a,(α,b) # ss)  seq ars"

definition lst :: "('a,'b) seq  'a"
 where "lst ss = (if snd ss = [] then fst ss else snd (last (snd ss)))"

text results on seqs
lemma seq_tail1: assumes seq: "(s,x#xs)  seq lars"
shows "(snd x,xs)  seq lars" and "(s,fst x,snd x)  lars" and "lst (s,x#xs) = lst (snd x,xs)"
proof -
 show "(snd x,xs) seq lars" using assms by (cases) auto
next
 show "(s,fst x,snd x)  lars"  using assms by (cases) auto
next
 show "lst (s,x#xs) = lst (snd x,xs)" using assms unfolding lst_def by (cases) auto
qed

lemma seq_chop: assumes "(s,ss@ts)  seq ars" shows "(s,ss)  seq ars" "(lst(s,ss),ts)  seq ars" proof -
 show "(s,ss)  seq ars" using assms proof (induct ss arbitrary: s)
  case Nil show ?case using seq.intros(1) by fast
 next
  case (Cons x xs) hence k:"(s,x#(xs@ts))  seq ars" by auto
  from Cons have "(snd x,xs)  seq ars" using seq_tail1(1) unfolding append.simps by fast
  thus ?case using seq.intros(2)[OF seq_tail1(2)[OF k]] by auto
 qed
next
 show "(lst(s,ss),ts)  seq ars" using assms proof (induct ss arbitrary:s)
  case Nil thus ?case unfolding lst_def by auto
 next
  case (Cons x xs)
  hence "(lst (snd x,xs),ts)  seq ars" using seq_tail1(1) unfolding append.simps by fast
  thus ?case unfolding lst_def by auto
 qed
qed

lemma seq_concat_helper:
assumes "(s,ls)  seq ars" and "ss2  seq ars" and "lst (s,ls) = fst ss2"
shows "(s,ls@snd ss2)  seq ars  (lst (s,ls@snd ss2) = lst ss2)"
using assms proof (induct ls arbitrary: s ss2 rule:list.induct)
 case Nil thus ?case unfolding lst_def by auto
 next
 case (Cons x xs)
 hence "(snd x,xs)  seq ars" and mem:"(s,fst x,snd x)  ars" and "lst (snd x,xs) = fst ss2"
  using seq_tail1[OF Cons(2)] Cons(4) by auto
 thus ?case using Cons seq.intros(2)[OF mem] unfolding lst_def by auto
qed

lemma seq_concat:
 assumes "ss1  seq ars" and "ss2  seq ars" and "lst ss1 = fst ss2"
 shows "(fst ss1,snd ss1@snd ss2)  seq ars" and "(lst (fst ss1,snd ss1@snd ss2) = lst ss2)"
 proof -
  show "(fst ss1,snd ss1@snd ss2)  seq ars" using seq_concat_helper assms by force
 next
  show "(lst (fst ss1,snd ss1@snd ss2) = lst ss2)"
   using assms surjective_pairing seq_concat_helper by metis
qed

text diagrams

definition diagram :: "('a,'b) lars  ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq  bool"
 where "diagram ars d = (let (τ,σ,σ',τ') = d in {σ,τ,σ',τ'}  seq ars 
   fst σ = fst τ  lst σ = fst τ'  lst τ = fst σ'  lst σ' = lst τ')"

definition labels :: "('a,'b) seq  'b list"
 where "labels ss = map fst (snd ss)"

definition D2 :: "'b rel  ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq  bool"
 where "D2 r d = (let (τ,σ,σ',τ') = d in D r (labels τ) (labels σ) (labels σ') (labels τ'))"

lemma lemma3_5_d: assumes "diagram ars (τ,σ,σ',τ')" and "diagram ars (υ,σ',σ'',υ')"
shows "diagram ars ((fst τ,snd τ@snd υ),σ,σ'',(fst τ'),snd τ'@snd υ')" proof -
 from assms have tau: "τ  seq ars" and upsilon: "υ  seq ars" and o: "lst τ = fst υ"
            and tau': "τ'  seq ars" and upsilon': "υ'  seq ars" and l: "lst τ' = fst υ'"
  unfolding diagram_def by auto
show ?thesis using assms seq_concat[OF tau' upsilon' l] seq_concat[OF tau upsilon o] unfolding diagram_def by auto
qed

lemma lemma3_5_d_v: assumes "diagram ars (τ,σ,σ',τ')" and "diagram ars (τ',υ,υ',τ'')"
shows "diagram ars (τ,(fst σ,snd σ@snd υ),(fst σ',snd σ'@snd υ'),τ'')" proof -
 from assms have d1: "diagram ars (σ,τ,τ',σ')" and d2: "diagram ars (υ,τ',τ'',υ')" unfolding diagram_def by auto
 show ?thesis using lemma3_5_d[OF d1 d2] unfolding diagram_def by auto
qed

lemma lemma3_5': assumes "trans r" and "irrefl r" and "D2 r (τ,σ,σ',τ')" and "D2 r (υ,σ',σ'',υ')"
shows "D2 r ((fst τ,snd τ@snd υ),σ,σ'',(fst τ'),snd τ'@snd υ')"
 using assms lemma3_5[OF assms(1,2)] unfolding labels_def D2_def by auto

lemma lemma3_5'_v: assumes "trans r" and "irrefl r" and "D2 r (τ,σ,σ',τ')" and "D2 r (τ',υ,υ',τ'')"
shows "D2 r (τ, (fst σ,snd σ@snd υ),(fst σ',snd σ'@snd υ'),τ'')" proof -
 from assms(3,4) have D1:"D2 r (σ,τ,τ',σ')" and D2: "D2 r (υ,τ',τ'',υ')"
  unfolding D2_def using mirror_D[OF assms(1,2)] by auto
 show ?thesis using lemma3_5'[OF assms(1,2) D1 D2] mirror_D[OF assms(1,2)] unfolding D2_def by auto
qed

lemma trivial_diagram: assumes "σ  seq ars" shows "diagram ars (σ,(fst σ,[]),(lst σ,[]),σ)"
 using assms seq.intros(1) unfolding diagram_def Let_def lst_def by auto

lemma trivial_D2: assumes "σ  seq ars" shows "D2 r (σ,(fst σ,[]),(lst σ,[]),σ)"
 using assms unfolding D2_def D_def labels_def using mul_eq_reflexive by auto

(* lift to combined concept *)
definition DD :: "('a,'b) lars  'b rel  ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq  bool"
 where "DD ars r d = (diagram ars d  D2 r d)"

lemma lemma3_5_DD: assumes "trans r" and "irrefl r" and "DD ars r (τ,σ,σ',τ')" and "DD ars r (υ,σ',σ'',υ')"
shows "DD ars r ((fst τ,snd τ@snd υ),σ,σ'',(fst τ'),snd τ'@snd υ')"
  using assms lemma3_5_d lemma3_5'[OF assms(1,2)] unfolding DD_def by fast

lemma lemma3_5_DD_v: assumes "trans r" and "irrefl r" and "DD ars r (τ,σ,σ',τ')" and "DD ars r (τ',υ,υ',τ'')"
shows "DD ars r (τ, (fst σ,snd σ@snd υ),(fst σ',snd σ'@snd υ'),τ'')"
  using assms lemma3_5_d_v lemma3_5'_v unfolding DD_def by fast

lemma trivial_DD: assumes "σ  seq ars" shows "DD ars r (σ,(fst σ,[]),(lst σ,[]),σ)"
 using assms trivial_diagram trivial_D2 unfolding DD_def by fast

lemma mirror_DD: assumes "trans r" and "irrefl r" and "DD ars r (τ,σ,σ',τ')" shows "DD ars r (σ,τ,τ',σ')"
 using assms mirror_D unfolding DD_def D2_def diagram_def by auto

text well-foundedness of rel r

definition measure :: "'b rel  ('a,'b) seq × ('a,'b) seq  'b multiset"
 where "measure r P = r|labels (fst P)| + r|labels (snd P)|"

definition pex :: "'b rel  (('a,'b) seq × ('a,'b) seq) rel"
 where "pex r = {(P1,P2). (measure r P1,measure r P2)  mul r}"

lemma wfi: assumes "relr = pex r" and "¬ wf (relr)" shows "¬ wf (mul r)" proof -
 have "¬ SN ((relr)¯)" using assms unfolding SN_iff_wf converse_converse by auto
 from this obtain s where "i. (s i, s (Suc i))  relr¯" unfolding SN_def SN_on_def by auto
 hence fact:"i. (measure r (s i), measure r (s (Suc i)))  (mul r)¯" unfolding assms(1) pex_def by auto
 have "¬ SN ((mul r)¯)" using chain_imp_not_SN_on[OF fact] unfolding SN_on_def by auto
 thus ?thesis unfolding SN_iff_wf converse_converse by auto
qed

lemma wf: assumes "trans r" and "wf r" shows "wf (pex r)" using wf_mul[OF assms] wfi by auto

text main result

definition peak :: "('a,'b) lars  ('a,'b) seq × ('a,'b) seq  bool"
 where "peak ars p = (let (τ,σ) = p in {τ,σ}  seq ars  fst τ = fst σ)"

definition local_peak :: "('a,'b) lars  ('a,'b) seq × ('a,'b) seq  bool"
 where "local_peak ars p = (let (τ,σ) = p in peak ars p  length (snd τ) = 1  length (snd σ) = 1)"

text proof of Theorem 3.7
lemma LD_imp_D: assumes "trans r" and "wf r" and "P. (local_peak ars P  ( σ' τ'. DD ars r (fst P,snd P,σ',τ')))"
and "peak ars P" shows "( σ' τ'. DD ars r (fst P,snd P,σ',τ'))" proof -
 have i: "irrefl r" using assms(1,2) acyclic_irrefl trancl_id wf_acyclic by metis
 have wf: "wf (pex r)" using wf[OF assms(1,2)] .
 show ?thesis using assms(4) proof (induct rule:wf_induct_rule[OF wf])
  case (1 P)
  obtain s τ σ where decompose:"P = (τ,σ)" and tau:"τ  seq ars" and sigma:"σ  seq ars"
   and tau_s: "fst τ = s" and sigma_s: "fst σ = s" using 1 unfolding peak_def by auto
  show ?case proof (cases "snd τ")
   case Nil from mirror_DD[OF assms(1) i trivial_DD[OF sigma]]
   show ?thesis using tau_s sigma_s Nil surjective_pairing unfolding decompose fst_conv snd_conv DD_def by metis
  next
   case (Cons β_step υ_step)
   hence tau_dec: "τ = (s,[β_step]@υ_step)" apply auto using tau_s surjective_pairing by metis
   hence tau2:" (s,[β_step]@υ_step)  seq ars" using tau by auto
   show ?thesis proof (cases "snd σ")
    case Nil from trivial_DD[OF tau]
    show ?thesis using tau_s sigma_s Nil surjective_pairing unfolding decompose fst_conv snd_conv DD_def by metis
   next
    case (Cons α_step ρ_step)
    hence sigma_dec: "σ = (s,[α_step]@ρ_step)" apply auto using sigma_s surjective_pairing by metis
    hence sigma2:"(s,[α_step]@ρ_step)  seq ars" using sigma by auto

    have alpha:"(s,[α_step])  seq ars" (is "  _")
     and rho: "(lst (s,[α_step]),ρ_step)  seq ars" (is "  _") using seq_chop[OF sigma2] by auto
    have beta:"(s,[β_step])  seq ars" (is "  _")
     and upsilon: "(lst (s,[β_step]),υ_step)  seq ars" (is "  _") using seq_chop[OF tau2] by auto
    have "local_peak ars (,)" using alpha beta unfolding