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 "∀k∈set_mset K.∃j∈set_mset J.(k,j)∈r" shows "set_mset K ⊆ dm r J" proof
 fix x assume "x∈set_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 "∀k∈set_mset K.∃j∈set_mset J.(k,j)∈r" proof
 fix k assume "k∈ set_mset K" thus "∃j∈set_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

text‹useful 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 "y∈set_mset M - set_mset N" shows "∃z∈set_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:"y∈set_mset M" and F3:"(x,y)∈r" unfolding dm_def ds_def by auto
  hence "∃ z ∈ set_mset N. (x,z)∈r" proof (cases "y∈set_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 local_peak_def peak_def by auto
    from this obtain κ μ where D:"DD ars r (?β,?α,κ,μ)" using assms(3) apply auto by metis
    hence kappa: "κ∈seq ars" and mu: "μ∈seq ars" unfolding DD_def diagram_def by auto
    have P_IH1: " peak ars (?υ,κ)" using upsilon kappa D unfolding DD_def diagram_def peak_def by auto
    have beta_ne: "labels ?β ≠ []" unfolding labels_def by auto
    have dec: "D r (labels ?β) (labels ?α) (labels κ) (labels μ)" using D unfolding DD_def D2_def by auto
    have x1:"((?υ,κ), (τ,?α)) ∈ pex r" using lemma3_6[OF assms(1) beta_ne dec]
      unfolding pex_def measure_def decompose labels_def tau_dec by (simp add: add.commute)
    have "(lexmax r (labels τ) + lexmax r (labels (?α)), lexmax r (labels τ) + lexmax r (labels σ)) ∈ mul_eq r" (is "(?l,?r) ∈ _")
     unfolding sigma_dec labels_def snd_conv list.map lexmax.simps diff_from_empty
     using assms(1) by (simp add: lemma2_6_2_a)
    hence "((?υ,κ),P) ∈ pex r" using x1 unfolding sigma_s pex_def measure_def decompose using mul_and_mul_eq_imp_mul[OF assms(1)] by auto
    from this obtain κ' υ' where IH1: "DD ars r (?υ,κ,κ',υ')" using 1(1)[OF _ P_IH1] unfolding decompose by auto
    hence kappa':"κ'∈seq ars" and upsilon': "υ'∈seq ars" using D unfolding DD_def diagram_def by auto
    have tau': "(fst μ,snd μ@(snd υ')) ∈ seq ars" (is "?τ' ∈ _") using seq_concat(1)[OF mu upsilon'] D IH1 unfolding DD_def diagram_def by auto
    have DIH1: "DD ars r (τ,?α,κ',?τ')" using lemma3_5_DD[OF assms(1) i D IH1] tau_dec by auto
    hence dec_dih1: "D r (labels τ) (labels ?α) (labels κ') (labels ?τ')" using DIH1 unfolding DD_def D2_def by simp

    have P_IH2: "peak ars (?τ',?ρ)" using tau' rho D unfolding DD_def diagram_def peak_def by auto
    have alpha_ne: "labels ?α ≠ []" unfolding labels_def by simp
    have "((?τ',?ρ),P) ∈ pex r" using lemma3_6_v[OF assms(1) i alpha_ne dec_dih1] unfolding pex_def measure_def decompose labels_def sigma_dec by auto
    from this obtain ρ' τ'' where IH2: "DD ars r (?τ',?ρ,ρ',τ'')" using 1(1)[OF _ P_IH2] by auto
    show ?thesis using lemma3_5_DD_v[OF assms(1) i DIH1 IH2] unfolding decompose fst_conv snd_conv sigma_dec by fast
   qed
  qed
 qed
qed

text ‹CR with unlabeling›
definition unlabel :: "('a,'b) lars ⇒ 'a rel"
 where "unlabel ars = {(a,c). ∃b. (a,b,c) ∈ ars}"

lemma step_imp_seq: assumes "(a,b) ∈ (unlabel ars)"
shows "∃ss ∈ seq ars. fst ss = a ∧ lst ss = b" proof -
 obtain α where step:"(a,α,b) ∈ ars" using assms unfolding unlabel_def by auto
 hence ss: "(a,[(α,b)]) ∈ seq ars" (is "?ss ∈ _") using seq.intros by fast
 have "fst ?ss = a" and "lst ?ss = b" unfolding lst_def by auto
 thus ?thesis using ss unfolding lst_def by fast
qed

lemma steps_imp_seq: assumes "(a,b) ∈ (unlabel ars)^*"
shows "∃ss ∈ seq ars. fst ss = a ∧ lst ss = b" using assms(1) proof
 fix n assume A: "(a,b) ∈ (unlabel ars)^^n" thus ?thesis proof (induct n arbitrary: a b ars)
 case 0 hence eq: "a = b" by auto
   have "(a,[]) ∈ seq ars" using seq.intros(1) by fast
  thus ?case using fst_eqD snd_conv lst_def eq by metis
 next
 case (Suc m)
  obtain c where steps: "(a,c) ∈ (unlabel ars)^^m" and step: "(c,b) ∈ (unlabel ars)" using Suc by auto
  obtain ss ts where ss1: "ss ∈ seq ars" and ss2:"fst ss = a"
   and ts1: "ts ∈ seq ars" and ts3:"lst ts = b" and eq: "lst ss = fst ts"
   using Suc steps step_imp_seq[OF step] by metis
 show ?case using seq_concat[OF ss1 ts1 eq] unfolding ss2 ts3 by force
qed
qed

lemma step_imp_unlabeled_step: assumes "(a,b,c) ∈ ars" shows "(a,c) ∈ (unlabel ars)"
 using assms unfolding unlabel_def by auto

lemma seq_imp_steps:
assumes "ss ∈ seq ars" and "fst ss = a" and "lst ss = b" shows "(a,b) ∈ (unlabel ars)^*" proof -
 from assms surjective_pairing obtain ls where "(a,ls) ∈ seq (ars)" and "lst (a,ls) = b" by metis
 thus ?thesis proof (induct ls arbitrary: a b rule:list.induct)
  case Nil thus ?case unfolding lst_def by auto
 next
  case (Cons x xs)
  have fst:"(a,fst x,snd x) ∈ ars" using Cons seq_tail1(2) surjective_pairing by metis
  have "(snd x,b) ∈ (unlabel ars)^*" using Cons seq_tail1(1,3) by metis
  thus ?case using step_imp_unlabeled_step[OF fst] by auto
 qed
qed

lemma seq_vs_steps: shows "(a,b) ∈ (unlabel ars)^* = (∃ss. fst ss = a ∧ lst ss = b ∧ ss ∈ seq ars)"
 using seq_imp_steps steps_imp_seq by metis

lemma D_imp_CR: assumes "∀P. (peak ars P ⟶ (∃ σ' τ'. DD ars r (fst P,snd P,σ',τ')))" shows "CR (unlabel ars)" proof
 fix a b c assume A: "(a,b) ∈ (unlabel ars)^*" and B: "(a,c) ∈ (unlabel ars)^*" show "(b,c) ∈ (unlabel ars)⇧↓" proof -
  obtain ss1 ss2 where " peak ars (ss1,ss2)" and b: "lst ss1 = b" and c: "lst ss2 = c"
   unfolding peak_def using A B unfolding seq_vs_steps by auto
  from this obtain ss3 ss4 where dia: "diagram ars (ss1,ss2,ss3,ss4)" using assms(1) unfolding DD_def apply auto using surjective_pairing by metis
  from dia obtain d where ss3: "ss3 ∈ seq ars" and ss4: "ss4 ∈ seq ars"
   and ss3_1: "fst ss3 = b" and ss3_2: "lst ss3 = d" and ss4_1: "fst ss4 = c" and ss4_2:"lst ss4 = d"
   using b c unfolding diagram_def by auto
  show ?thesis using seq_imp_steps[OF ss3 ss3_1 ss3_2] seq_imp_steps[OF ss4 ss4_1 ss4_2] by auto
 qed
qed

definition LD :: "'b set ⇒ 'a rel ⇒ bool"
 where "LD L ars = (∃ (r:: ('b rel)) (lrs::('a,'b) lars). (ars = unlabel lrs) ∧ trans r ∧ wf r ∧ (∀P. (local_peak lrs P ⟶ (∃ σ' τ'. (DD lrs r (fst P,snd P,σ',τ'))))))"

lemma sound: assumes "LD L ars" shows "CR ars"
 using assms LD_imp_D D_imp_CR unfolding LD_def by metis

subsubsection ‹Application: Newman's Lemma›
lemma measure:
assumes lab_eq: "lrs = {(a,c,b). c = a ∧ (a,b) ∈ ars}" and "(s,(α,t) # ss) ∈ seq lrs"
shows "set (labels (t,ss)) ⊆ ds ((ars^+)¯) {α}" using assms(2) proof (induct ss arbitrary: s α t )
 case Nil thus ?case unfolding labels_def by auto
next
 case (Cons x xs)
 from this obtain β u where x:"x = (β,u)" using surjective_pairing by metis
 have t: "trans ((ars⇧+)¯)" by (metis trans_on_converse trans_trancl)
 from Cons(1) x have s0: "(s, α, t) ∈ lrs" and cs:"(t,(β,u)#xs) ∈ seq lrs" using Cons.prems seq_tail1(1) snd_conv fst_conv seq_tail1(2) by auto
 have ih: "set (labels (u, xs)) ⊆ ds ((ars^+)¯) {β}" using Cons(1)[OF cs] by auto
 have key: "{β} ⊆ ds ((ars^+)¯) {α}" using s0 cs seq_tail1(2)[OF cs] unfolding ds_def lab_eq by auto
 show ?case using ih subset_imp_ds_subset[OF t key] key unfolding x labels_def by auto
qed

lemma newman: assumes "WCR ars" and "SN ars" shows "CR ars"  proof -
 from assms obtain L where "L =  {a . ∃ b. (a,b) ∈ ars}" by auto
 from assms obtain lrs where lab_eq: "(lrs  = {(a,c,b). c = a ∧ (a,b) ∈ ars})" by auto

 have lab: "ars = unlabel lrs" unfolding unlabel_def lab_eq by auto
 have t: "trans ((ars⇧+)¯)" using trans_on_converse trans_trancl by auto
 have w: "wf ((ars^+)¯)" using assms(2) wf_trancl trancl_converse unfolding SN_iff_wf by metis
 have ps: "∀P. (local_peak lrs P --> (∃ σ' τ'. DD lrs ((ars^+)¯) (fst P,snd P,σ',τ')))" proof
  fix P show "local_peak lrs P --> (∃ σ' τ'. DD lrs ((ars^+)¯) (fst P,snd P,σ',τ'))" proof
   assume A: "local_peak lrs P" show "(∃ σ' τ'. DD lrs ((ars^+)¯) (fst P,snd P,σ',τ'))" (is "?DD") proof -
    from lab_eq have lab: "ars = unlabel lrs" unfolding unlabel_def by auto
    from A obtain τ σ where ts: "{τ,σ} ⊆ seq lrs" and l1: "length (snd τ) = 1" and l2: "length (snd σ) = 1" and P: "P = (τ,σ)"
     and p: "fst τ = fst σ" unfolding local_peak_def peak_def by auto

    from l1 obtain β b where 1: "snd τ = [(β,b)]" by(auto simp add: length_Suc_conv)
    from this obtain a where tau: "τ = (a,[(β,b)])" by (metis surjective_pairing)
    hence alb: "(a,β,b) ∈ lrs" using ts by (metis fst_conv insert_subset seq_tail1(2) snd_conv)
    have ab: "(a,b) ∈ ars" and a_eq: "a = β" using alb unfolding lab_eq by auto

    from l2 obtain α c where 2: "snd σ = [(α,c)]" by(auto simp add: length_Suc_conv)
    hence sigma: "σ = (a,[(α,c)])" using ts by (metis fst_conv p prod.collapse tau)
    hence alc: "(a,α,c) ∈ lrs" using ts by (metis fst_conv insert_subset seq_tail1(2) snd_conv)
    hence ac: "(a,c) ∈ ars" and a_eq: "a = α" using alb unfolding lab_eq by auto

    from tau sigma have fl: "fst τ = a ∧ fst σ = a ∧ lst τ = b ∧ lst σ = c" unfolding lst_def by auto
    from ab ac obtain d where "(b,d) ∈ ars^*" and "(c,d) ∈ ars^*" using assms(1) by auto
    from this obtain σ' τ' where sigma': "σ' ∈ seq lrs" and sigma'1: "fst σ' = b" and "lst σ' = d"
                           and  tau':"τ' ∈ seq lrs" and "fst τ' = c" and "lst τ' = d" using steps_imp_seq unfolding lab by metis
    hence d:"diagram lrs (fst P, snd P, σ', τ')" using P A ts fl unfolding local_peak_def peak_def diagram_def by auto

    have s1:"(a,(β,b)# snd σ') ∈ seq lrs" using ‹fst σ' = b› seq.intros(2)[OF alb] sigma' by auto
    have vv: "set (labels σ') ⊆ ds ((ars^+)¯) {β}"  using measure[OF lab_eq s1] by (metis ‹fst σ' = b› surjective_pairing)
    have s2:"(a,(α,c)# snd τ') ∈ seq lrs" using ‹fst τ' = c› seq.intros(2)[OF alc] tau' by auto
    hence ww: "set (labels τ') ⊆ ds ((ars^+)¯) {α}" using measure[OF lab_eq] s2 by (metis ‹fst τ' = c› surjective_pairing)
    from w have i: "irrefl ((ars^+)¯)" by (metis SN_imp_acyclic acyclic_converse acyclic_irrefl assms(2) trancl_converse)
    from vv ww have ld: "LD' ((ars^+)¯) β α (labels σ') [] [] (labels τ') [] []" unfolding LD'_def LD_1'_def by auto
    have D: "D ((ars^+)¯) (labels (fst P)) (labels (snd P)) (labels σ') (labels τ')" using proposition3_4[OF t i ld] unfolding P sigma tau lst_def labels_def by auto

    from d D have "DD lrs ((ars^+)¯) (fst P, snd P, σ', τ')" unfolding DD_def D2_def by auto
    thus ?thesis by fast
   qed
  qed
 qed
 have "LD L ars" using lab t w ps unfolding LD_def by fast
 thus ?thesis using sound by auto
qed

subsection ‹Conversion Version›
text ‹This section follows~\<^cite>‹"vO08a"›.›
text ‹auxiliary results on multisets›
lemma mul_eq_add_right: "(M,M+P) ∈ mul_eq r" proof -
 have "M = M + {#}" "set_mset {#} ⊆ dm r P" by auto
 thus ?thesis unfolding mul_eq_def by fast
qed

lemma mul_add_right: assumes "(M,N) ∈ mul r" shows "(M,N+P) ∈ mul r" proof -
 from assms obtain I J K where "M = I + K" "N = I + J" "set_mset K ⊆ dm r J" "J ≠ {#}" unfolding mul_def by auto
 hence b: "M = I + K" "N + P = I + (J + P)" "set_mset K ⊆ ds r (set_mset J ∪ set_mset P)" "J+P ≠ {#}" unfolding dm_def lemma2_6_1_set using union_assoc by auto
 hence "set_mset K ⊆ ds r (set_mset (J+P ))" by auto
 thus ?thesis using b unfolding mul_def unfolding dm_def by fast
qed

lemma mul_eq_and_ds_imp_ds:
assumes t: "trans r" and "(M,N) ∈ mul_eq r" and "set_mset N ⊆ ds r S"
shows "set_mset M ⊆ ds r S" proof -
 from assms obtain I J K where a: "M = I + K" and "N = I + J" and c: "set_mset K ⊆ dm r J" unfolding mul_eq_def by auto
 hence k1:"set_mset I ⊆ ds r S" "set_mset J ⊆ ds r S" using assms by auto
 hence "ds r (set_mset J) ⊆ ds r S"  using subset_imp_ds_subset[OF t] by auto
 thus ?thesis using k1 a c unfolding dm_def by auto
qed

lemma lemma2_6_2_set: assumes "S ⊆ T" shows "ds r S ⊆ ds r T" using assms unfolding ds_def by auto

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

lemma mul_add_mul_eq_imp_mul: assumes "(M,N) ∈ mul r" and "(P,Q) ∈ mul_eq r" shows "(M+P,N+Q) ∈ mul r" proof -
 from assms(1) obtain I J K where a:"M = I + K" "N = I + J" "set_mset K ⊆ dm r J" "J ≠ {#}" unfolding mul_def by auto
 from assms(2) obtain I2 J2 K2 where b:"P = I2 + K2" "Q = I2 + J2" "set_mset K2 ⊆ dm r J2" unfolding mul_eq_def by auto
 have "M + P = (I + I2) + (K + K2)" using a b union_commute union_assoc by metis
 moreover have "N + Q = (I + I2) + (J + J2)" using a b union_commute union_assoc by metis
 moreover have "set_mset (K + K2) ⊆ dm r (J + J2)"  using a b unfolding lemma2_6_1_multiset by auto
 ultimately show ?thesis using a b unfolding mul_def by fast
qed

text ‹labeled conversion›
type_synonym ('a,'b) conv = "('a × ((bool × 'b × 'a) list))"

inductive_set conv :: "('a,'b) lars ⇒ ('a,'b) conv set" for ars
where "(a,[]) ∈ conv ars"
    | "(a,α,b) ∈ ars ⟹ (b,ss) ∈ conv ars ⟹ (a,(True,α,b) # ss) ∈ conv ars"
    | "(b,α,a) ∈ ars ⟹ (b,ss) ∈ conv ars ⟹ (a,(False,α,b) # ss) ∈ conv ars"

definition labels_conv :: "('a,'b) conv ⇒ 'b list"
 where "labels_conv c = map (λq. (fst (snd q))) (snd c)"

definition measure_conv :: "'b rel ⇒ ('a,'b) conv ⇒ 'b multiset"
 where "measure_conv r c = lexmax r (labels_conv c)"

fun lst_conv :: "('a,'b) conv ⇒ 'a"
  where "lst_conv (s,[]) = s"
 | "lst_conv (s,(d,α,t) # ss) = lst_conv (t,ss)"

definition local_diagram1 :: "('a,'b) lars ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ bool"
 where "local_diagram1 ars β α σ1 σ2 σ3 =
  (local_peak ars (β,α) ∧ {σ1,σ2,σ3} ⊆ seq ars ∧ lst β = fst σ1 ∧ lst σ1 = fst σ2 ∧ lst σ2 = fst σ3)"

definition LDD1 :: "('a,'b) lars ⇒ 'b rel ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ bool"
 where "LDD1 ars r β α σ1 σ2 σ3 =  (local_diagram1 ars β α σ1 σ2 σ3 ∧
  LD_1' r (hd (labels β)) (hd (labels α)) (labels σ1) (labels σ2) (labels σ3))"

definition LDD :: "('a,'b) lars ⇒ 'b rel ⇒ ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq × ('a,'b) seq ⇒ bool"
 where "LDD ars r d = (let (β,α,σ1,σ2,σ3,τ1,τ2,τ3) = d in LDD1 ars r β α σ1 σ2 σ3 ∧ LDD1 ars r α β τ1 τ2 τ3 ∧ lst σ3 = lst τ3)"

definition local_triangle1 :: "('a,'b) lars ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) conv ⇒ ('a,'b) seq ⇒ ('a,'b) conv ⇒ bool"
 where "local_triangle1 ars β α σ1 σ2 σ3 =
  (local_peak ars (β,α) ∧ σ2 ∈ seq ars ∧ {σ1,σ3} ⊆ conv ars ∧ lst β = fst σ1 ∧ lst_conv σ1 = fst σ2 ∧ lst σ2 = fst σ3)"

definition LT1 :: "('a,'b) lars ⇒ 'b rel ⇒ ('a,'b) seq ⇒ ('a,'b) seq ⇒ ('a,'b) conv ⇒ ('a,'b) seq ⇒ ('a,'b) conv ⇒ bool"
 where "LT1 ars r β α σ1 σ2 σ3 = (local_triangle1 ars β α σ1 σ2 σ3 ∧
  LD_1' r (hd (labels β)) (hd (labels α)) (labels_conv σ1) (labels σ2) (labels_conv σ3))"

definition LT :: "('a,'b) lars ⇒ 'b rel ⇒ ('a,'b) seq × ('a,'b) seq × ('a,'b) conv × ('a,'b) seq × ('a,'b) conv × ('a,'b) conv × ('a,'b) seq × ('a,'b) conv ⇒ bool"
 where "LT ars r t = (let (β,α,σ1,σ2,σ3,τ1,τ2,τ3) = t in LT1 ars r β α σ1 σ2 σ3 ∧ LT1 ars r α β τ1 τ2 τ3 ∧ lst_conv σ3 = lst_conv τ3)"

lemma conv_tail1: assumes conv: "(s,(d,α,t)#xs) ∈ conv ars"
shows "(t,xs) ∈ conv ars" and "d ⟹ (s,α,t) ∈ ars" and "¬d ⟹ (t,α,s) ∈ ars" and "lst_conv (s,(d,α,t)#xs) = lst_conv (t,xs)" proof -
 show "(t,xs) ∈ conv ars" using assms by (cases) auto
 show "d ⟹ (s,α,t) ∈ ars" using assms by (cases) auto
 show "¬d ⟹ (t,α,s) ∈ ars" using assms by (cases) auto
 show "lst_conv (s,(d,α,t)#xs) = lst_conv (t,xs)" unfolding lst_conv.simps by auto
qed

lemma conv_chop: assumes "(s,ss1@ss2) ∈ conv ars" shows "(s,ss1) ∈ conv ars" "(lst_conv (s,ss1),ss2) ∈ conv ars" proof -
 show "(s,ss1) ∈ conv ars" using assms proof (induct ss1 arbitrary: s)
  case Nil thus ?case using conv.intros by fast
 next
  case (Cons t' ts) from this obtain d α t where dec: "t' = (d,α,t)" using prod_cases3 by metis
  from Cons have "(s, t' # ts @ ss2) ∈ conv ars" by auto
  hence "(t, ts @ ss2) ∈ conv ars" and d1: "d ⟹ (s,α,t) ∈ ars" and d2:"¬d ⟹ (t,α,s) ∈ ars" using conv_tail1(1-3) unfolding dec by auto
  hence "(t, ts) ∈ conv ars" using Cons by auto
  thus ?case unfolding dec using Cons conv.intros d1 d2 by (cases d) auto
 qed
 show "(lst_conv (s,ss1),ss2) ∈ conv ars" using assms proof (induct ss1 arbitrary:s)
  case Nil thus ?case using conv.intros unfolding last.simps by auto
 next
  case (Cons t' ts) from this obtain d α t where dec: "t' = (d,α,t)" using prod_cases3 by metis
  from Cons have "(s, t' # ts @ ss2) ∈ conv ars" by auto
  hence "(snd (snd t'), ts @ ss2) ∈ conv ars" using conv_tail1(1) unfolding dec by auto
  thus ?case using Cons(1) unfolding dec last.simps by auto
 qed
qed

lemma conv_concat_helper:
assumes "(s,ls) ∈ conv ars" and "ss2 ∈ conv ars" and "lst_conv (s,ls) = fst ss2"
shows "(s,ls@snd ss2) ∈ conv ars ∧ (lst_conv (s,ls@snd ss2) = lst_conv 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) from this obtain d α t where dec: "x = (d,α,t)" using prod_cases3 by metis
 hence tl: "(t,xs) ∈ conv ars" and d1:"d ⟹ (s,α,t) ∈ ars" and d2: "¬d ⟹ (t,α,s) ∈ ars" and lst:"lst_conv (t,xs) = fst ss2"
  using conv_tail1 Cons(2) Cons(4) by auto
 have "(t,xs@snd ss2) ∈ conv ars" and lst: "lst_conv (t,xs@snd ss2) = lst_conv ss2"  using Cons(1)[OF tl Cons(3) lst] by auto
 thus ?case using conv.intros d1 d2 unfolding dec lst_conv.simps by (cases d) auto
qed

lemma conv_concat:
 assumes "ss1 ∈ conv ars" and "ss2 ∈ conv ars" and "lst_conv ss1 = fst ss2"
 shows "(fst ss1,snd ss1@snd ss2) ∈ conv ars" and "(lst_conv (fst ss1,snd ss1@snd ss2) = lst_conv ss2)"
 proof -
  show "(fst ss1,snd ss1@snd ss2) ∈ conv ars" using conv_concat_helper assms by force
 next
  show "(lst_conv (fst ss1,snd ss1@snd ss2) = lst_conv ss2)"
   using assms surjective_pairing conv_concat_helper by metis
qed

lemma conv_concat_labels:
assumes "ss1 ∈ conv ars" and "ss2 ∈ conv ars" and "set (labels_conv ss1) ⊆ S" and "set (labels_conv ss2) ⊆ T"
shows "set (labels_conv (fst ss1,snd ss1@snd ss2)) ⊆ S ∪ T" using assms unfolding labels_conv_def by auto

lemma seq_decompose:
assumes "σ ∈ seq ars" and "labels σ = σ1'@σ2'"
shows "∃ σ1 σ2. ({σ1,σ2} ⊆ seq ars ∧ σ = (fst σ1,snd σ1@snd σ2) ∧ lst σ1 = fst σ2 ∧ lst σ2 = lst σ ∧ labels σ1 = σ1' ∧ labels σ2 = σ2')" proof -
 obtain s ss where σ_dec: "σ = (s,ss)" using assms(1) surjective_pairing by metis
 show ?thesis using assms unfolding σ_dec proof (induct ss arbitrary: s σ1' σ2' rule:list.induct)
 case Nil thus ?case unfolding labels_def lst_def by auto
next
 case (Cons x xs)
  have step: "(s,x) ∈ ars" and x:"(snd x,xs) ∈ seq ars" using seq_tail1[OF Cons(2)] surjective_pairing by auto
  hence steps: "(s,[x]) ∈ seq ars" by (metis Cons(2) append_Cons append_Nil seq_chop(1))
  from Cons(3) have a:"fst x#labels (snd x,xs) = σ1'@σ2'" unfolding labels_def snd_conv by auto
  show ?case proof (cases "σ1'=[]")
   case True
   from a True obtain l ls where σ2'_dec: "σ2' = l#ls" and y1:"fst x = l" and y2:"labels (snd x,xs) = []@ls" by auto
   obtain σ1 σ2 where ih: "σ1 ∈ seq ars" "σ2 ∈ seq ars" "(snd x, xs) = (fst σ1, snd σ1 @ snd σ2)" "lst σ1 = fst σ2"
    "labels σ1 = []" "labels σ2 = ls" using Cons(1)[OF x y2] by blast
   hence c:"fst (snd x,xs) = fst σ1" by auto

   have 1: "σ1 = (snd x,[])" using ih unfolding labels_def apply auto by (metis surjective_pairing)
   hence 2: "snd x = fst σ1" "xs = snd σ2" using ih by auto
   have 3: "snd x = fst σ2" using ih 1 unfolding lst_def by auto
   have "σ2 = (snd x,xs)" using x 1 2 3 surjective_pairing by metis
   hence l:"lst (s, [x]) = fst σ2" unfolding lst_def by auto
   have m:"{(s,[]), (s,x# snd σ2)} ⊆ seq ars"  (is "{?σ1,?σ2} ⊆ _") using seq.intros(1) seq_concat(1)[OF steps _ l] ih by auto
   moreover have "(s, x # xs) = (fst ?σ1, snd ?σ1 @ snd ?σ2)" using m 2 by auto
   moreover have "lst ?σ1 = fst ?σ2" using m unfolding lst_def by auto
   moreover have "lst ?σ2 = lst (s,x#xs)" unfolding lst_def using 2 3 by auto
   moreover have "labels (s,[]) = σ1'" unfolding labels_def using True by auto
   moreover have "labels ?σ2 = σ2'" using ih y1 unfolding σ2'_dec labels_def by auto
   ultimately show ?thesis by metis
  next
   case False from False obtain l ls where σ1'_dec:"σ1' = l#ls" using list.exhaust by auto
   hence y1:"fst x = l" and y2:"labels (snd x,xs) = ls @ σ2'" using a by auto
   obtain σ1 σ2 where ih: "σ1 ∈ seq ars" "σ2 ∈ seq ars" "(snd x, xs) = (fst σ1, snd σ1 @ snd σ2)"
    "lst σ1 = fst σ2" "lst σ2 = lst (snd x, xs)" "labels σ1 = ls" "labels σ2 = σ2'" using  Cons(1)[OF x y2] by blast
   hence "{(s,x# snd σ1),σ2} ⊆ seq ars" (is "{?σ1,_} ⊆ seq ars") using seq_concat(1)[OF steps] ih unfolding lst_def by auto
   moreover have "(s,x#xs) = (fst ?σ1,snd ?σ1@snd σ2)" using ih by auto
   moreover have "lst ?σ1 = fst σ2" using ih unfolding lst_def by auto
   moreover have "lst σ2 = lst (s, x # xs)" using ih unfolding lst_def by auto
   moreover have "labels ?σ1 = σ1'" using ih σ1'_dec y1 unfolding labels_def by auto
   moreover have "labels σ2 = σ2'" using ih by auto
   ultimately show ?thesis by blast
  qed
 qed
qed

lemma seq_imp_conv:
assumes "(s,ss) ∈ seq ars"
shows "(s,map (λstep. (True,step)) ss) ∈ conv ars ∧
       lst_conv (s,map (λstep.(True,step)) ss) = lst (s,ss) ∧
       labels (s,ss) = labels_conv (s,map (λstep.(True,step)) ss)"
using assms proof (induct ss arbitrary: s rule:list.induct )
 case Nil show ?case  unfolding lst_def labels_def labels_conv_def apply auto using conv.intros by fast
next
 case (Cons t' ts) have t'_dec: "t' = (fst t',snd t')" using surjective_pairing by auto
  have step: "(s,fst t',snd t') ∈ ars" and x:"(snd t',ts) ∈ seq ars" using seq_tail1[OF Cons(2)] by auto
  have y1:"(snd t', map (Pair True) ts) ∈ conv ars" and
       y2: "lst (snd t', ts) = lst_conv (snd t', map (Pair True) ts)" and
       y3: "labels (snd t', ts) = labels_conv (snd t', map (Pair True) ts)" using Cons(1)[OF x] by auto
  have k: "(s,(True,fst t',snd t')#map (Pair True) ts) ∈ conv ars" using step y1 conv.intros by fast
  moreover have "lst (s,(fst t',snd t')#ts) = lst_conv (s, map (Pair True) ((fst t',snd t')#ts))" using y2 unfolding list.map lst_def lst_conv.simps by auto
  moreover have "labels (s,(fst t',snd t')#ts) = labels_conv (s,map (Pair True) ((fst t',snd t')#ts))" using y3 unfolding list.map labels_def labels_conv_def by auto
  ultimately show ?case by auto
qed

fun conv_mirror :: "('a,'b) conv ⇒ ('a,'b) conv"
 where "conv_mirror σ = (let (s,ss) = σ in case ss of
             [] ⇒ (s,ss)
         | x#xs ⇒ let (d,α,t) = x in
                   (fst (conv_mirror (t,xs)),snd (conv_mirror (t,xs))@[(¬d,α,s)]))"

lemma conv_mirror: assumes "σ ∈ conv ars"
shows "conv_mirror σ ∈ conv ars ∧
      set (labels_conv (conv_mirror σ)) = set (labels_conv σ) ∧
      fst σ = lst_conv (conv_mirror σ) ∧
      lst_conv σ = fst (conv_mirror σ)" proof -
 from assms obtain s ss where σ_dec: "σ = (s,ss)" using surjective_pairing by metis
 show ?thesis using assms unfolding σ_dec proof (induct ss arbitrary:s rule:list.induct)
  case Nil thus ?case using conv.intros  conv_mirror.simps by auto
 next
  case (Cons t' ts) from this obtain d α t where t'_dec: "t' = (d,α,t)" by (metis prod_cases3)
  have 1:"(t, ts) ∈ conv ars" and 2: "d ⟹ (s,α,t) ∈ ars" and 3: "¬d ⟹ (t,α,s) ∈ ars"  and 4:"lst_conv (s,t'#ts) = lst_conv (t,ts)"
   using Cons(2) conv_tail1 unfolding t'_dec by auto
  have r: "(t,[(¬d,α,s)]) ∈ conv ars" using 2 3 conv.intros(3)[OF _ conv.intros(1)] conv.intros(2)[OF _ conv.intros(1)] by (cases d) auto
  have "conv_mirror (s,t'#ts) ∈ conv ars" using conv_concat[OF _ r ] Cons(1)[OF 1] t'_dec by auto
  moreover have "set (labels_conv (conv_mirror (s, t' # ts))) = set (labels_conv (s, t' # ts))" using Cons(1)[OF 1] unfolding labels_conv_def t'_dec by auto
  moreover have "fst (s, t' # ts) = lst_conv (conv_mirror (s, t' # ts))" using t'_dec Cons(1)[OF 1] conv_concat(2)[OF _ r] by auto
  moreover have "lst_conv (s, t' # ts) = fst (conv_mirror (s, t' # ts))" using t'_dec 4 Cons(1)[OF 1] by auto
  ultimately show ?case by auto
 qed
qed

lemma DD_subset_helper:
assumes t:"trans r" and "(r|τ@σ'|, r|τ| + r|σ| ) ∈ mul_eq r" and "set_mset (r|τ| + r|σ| ) ⊆ ds r S"
shows "set_mset r|σ'| ⊆ ds r S" proof -
  from assms have d: "(r|τ| + r|σ'| -s dl r (τ) , r|τ| + r|σ| ) ∈ mul_eq r" unfolding lemma3_2_2 by auto
  from assms have assm:"set_mset (r|τ| + r|σ| ) ⊆ ds r S" unfolding measure_def by auto
  hence tau:"ds r (set_mset r|τ| ) ⊆ ds r S" using subset_imp_ds_subset[OF t] by auto
  have "set_mset (r|τ| + (r|σ'| -s dl r τ)) ⊆ ds r S" using mul_eq_and_ds_imp_ds[OF t d assm] by auto
  hence "set_mset (r|σ'| -s ds r (set τ)) ⊆ ds r S" unfolding dl_def by auto
  hence "set_mset (r|σ'| -s ds r (set τ)) ∪ ds r (set τ) ⊆ ds r S" using tau by (metis t dl_def dm_def le_sup_iff lemma3_2_1)
  thus ?thesis unfolding diff_def by auto
qed

lemma DD_subset_ds:
assumes t:"trans r" and DD: "DD ars r (τ,σ,σ',τ')" and "set_mset (measure r (τ,σ)) ⊆ ds r S" shows "set_mset (measure r (σ',τ')) ⊆ ds r S" proof -
 have d1:"(r|labels τ @ labels σ'|, r|labels τ| + r|labels σ| ) ∈ mul_eq r" using DD unfolding DD_def D2_def D_def by auto
 have d2:"(r|labels σ @ labels τ'|, r|labels σ| + r|labels τ| ) ∈ mul_eq r" using DD unfolding DD_def D2_def D_def
  by (auto simp: union_commute)
 show ?thesis using DD_subset_helper[OF t d1] DD_subset_helper[OF t d2] assms(3) unfolding measure_def by auto
qed

lemma conv_imp_valley:
assumes t: "trans r"
and IH: "!!y . ((y,((s,[α_step]@ρ_step),(s,[β_step]@υ_step))) ∈ pex r ⟹ peak ars y ⟹ ∃σ' τ'. DD ars r (fst y, snd y, σ', τ'))" (is "!!y. ((y,?P) ∈ _ ⟹ _ ⟹ _)")
and "δ1 ∈ conv ars"
and "set_mset (measure_conv r δ1) ⊆ dm r M"
and "(M,{#fst α_step,fst β_step#}) ∈ mul_eq r"
shows "∃ σ τ. ({σ,τ} ⊆ seq ars ∧ fst σ = fst δ1 ∧ fst τ = lst_conv δ1 ∧ lst σ = lst τ ∧ set_mset (measure r (σ,τ)) ⊆ dm r M)" proof -
 from assms obtain s ss where sigma1: "δ1 = (s,ss)" using surjective_pairing by metis
 show ?thesis using assms(3,4) unfolding sigma1 proof (induct ss arbitrary: s rule:list.induct)
  case Nil
  hence "(s,[]) ∈ seq ars" using seq.intros(1) by fast
  moreover have "set_mset (measure r ((s,[]),(s,[]))) ⊆ dm r M" unfolding measure_def labels_def by auto
  ultimately show ?case by auto
 next
  case (Cons t' ts) obtain d β t where dec: "t' = (d,β,t)" using surjective_pairing by metis
  hence dic: "{β} ⊆ ds r (set_mset M)" using Cons(3) unfolding dec measure_conv_def labels_conv_def dm_def by auto
  have one:"ds r {β} ⊆ dm r M " unfolding dm_def using subset_imp_ds_subset[OF t dic] by auto
  have "set_mset (measure_conv r (t,ts) -s ds r {β})  ⊆ dm r M" using Cons(3) unfolding measure_conv_def labels_conv_def dec by auto
  hence "set_mset (measure_conv r (t,ts)) ⊆ dm r M ∪ ds r {β}" unfolding set_mset_def diff_def by auto
  hence ts2: "set_mset (measure_conv r (t,ts)) ⊆ dm r M" using dic one by auto
  from Cons(2) have ts: "(t,ts) ∈ conv ars" unfolding dec using conv_tail1(1) by fast
  from Cons(1)[OF ts ts2] obtain σ' τ where
   ih:"{σ', τ} ⊆ seq ars ∧ fst σ' = fst (t,ts) ∧ fst τ = lst_conv (t, ts) ∧ lst σ' = lst τ ∧ set_mset (measure r (σ',τ)) ⊆ dm r M" by metis
  have diff:"!!x. x ∈# r|map fst (snd σ')|-sds r {β} ⟹ x ∈# r|map fst (snd σ')|"
    by simp
  show ?case proof (cases d)
   case True hence step:"(s,β,t) ∈ ars" using conv_tail1(2) Cons(2) unfolding dec by auto
   have "(s,(β,t)# snd σ') ∈ seq ars" (is "?σ ∈ _") using seq.intros(2)[OF step] using ih(1) by auto
   hence "{?σ,τ} ⊆ seq ars" using ih by auto
   moreover have "(fst ?σ) = fst (s, t' # ts)" by auto
   moreover have "fst τ = lst_conv (s, t' # ts)" using ih unfolding dec lst_conv.simps by auto
   moreover have "lst ?σ = lst τ" by (metis ‹(s, (β, t) # snd σ') ∈ seq ars› fst_conv ih seq_tail1(3) snd_conv surjective_pairing)
   moreover have "set_mset (measure r (?σ,τ)) ⊆ dm r M" using diff ih dic unfolding measure_def labels_def dm_def by auto
   ultimately show ?thesis by blast
  next
   case False hence step:"(t,β,s) ∈ ars" using conv_tail1(3) Cons(2) unfolding dec by auto
   hence "(t,[(β,s)]) ∈ seq ars" using seq.intros by metis
   hence p:"peak ars ((t,[(β,s)]),σ')" (is "peak ars ?y") using seq.intros unfolding peak_def using ih by auto
   hence mp: "set_mset (measure r ?y) ⊆ ds r (set_mset M)" using ih dic unfolding measure_def labels_def dm_def
     by simp
   hence ne: "M ≠ {#}" using dec dic unfolding dm_def ds_def by auto
   hence x:"(measure r ?y,M) ∈ mul r" using mp unfolding dm_def mul_def apply auto by (metis add_0)
   have "({#fst α_step#}+{#fst β_step#},measure r ?P) ∈ mul_eq r" unfolding assms(2) measure_def labels_def apply auto
    unfolding union_lcomm union_assoc[symmetric]  using mul_eq_add_right[where M="{#fst α_step#}+{#fst β_step#}"] unfolding union_assoc by auto
   hence  "(M,measure r ?P) ∈ mul_eq r" using assms(5) mul_eq_trans t by (auto simp: add_mset_commute)
   hence w:"(?y,?P) ∈ pex r" unfolding assms(1) pex_def using mul_and_mul_eq_imp_mul[OF t x] by auto
   obtain σ'' τ'' where DD:"DD ars r ((t,[(β,s)]),σ',σ'',τ'')" using IH[OF w p] by auto
   have sigma: "σ'' ∈ seq ars" "fst σ'' = fst (s, t' # ts)" "lst σ'' = lst τ''" using DD unfolding DD_def diagram_def lst_def by auto
   have tau'': "τ'' ∈ seq ars" and eq: "lst τ = fst τ''" using DD  unfolding DD_def diagram_def using ih by auto
   have tau:"(fst τ,snd τ @ snd τ'') ∈ seq ars" (is "?τ''' ∈ _") and "lst τ'' = lst (fst τ,snd τ@ snd τ'')" using seq_concat[OF _ tau'' eq] ih by auto
   hence tau2: "fst ?τ''' = lst_conv (s,t'#ts)" "lst σ'' = lst ?τ'''" using DD ih unfolding DD_def diagram_def dec lst_conv.simps by auto
   have "set_mset (measure r (σ'',τ'')) ⊆ ds r (set_mset M)" using DD_subset_ds[OF t DD mp] unfolding measure_def by auto
   hence "set_mset (r|labels σ''| + r|labels τ| + (r|labels τ''| -s (dl r (labels τ)) )) ⊆ dm r M" using ih unfolding measure_def dm_def diff_def by auto
   hence fin: "set_mset (measure r (σ'',?τ''')) ⊆ dm r M"  unfolding measure_def labels_def apply auto unfolding lemma3_2_2 by auto
   show ?thesis using sigma tau tau2 fin by blast
  qed
 qed
qed

lemma labels_multiset: assumes "length (labels σ) ≤ 1" and "set (labels σ) ⊆ {α}" shows "(r|labels σ|, {#α#}) ∈ mul_eq r"  proof (cases "snd σ")
 case Nil hence "r|labels σ| = {#}" unfolding labels_def by auto
 thus ?thesis unfolding mul_eq_def by auto
next
 case (Cons x xs) hence l:"length (labels σ) = 1" using assms(1) unfolding labels_def by auto
 from this have "labels σ ≠ []" by auto
 from this obtain a as where "labels σ = a#as" using neq_Nil_conv by metis
 hence leq: "labels σ = [a]" using l by auto
 hence "set (labels σ) = {α}" using assms(2) by auto
 hence "(r|labels σ| ) = {#α#}" unfolding leq lexmax.simps diff_def by auto
 thus ?thesis using mul_eq_reflexive by auto
qed

lemma decreasing_imp_local_decreasing:
assumes t:"trans r" and i:"irrefl r" and DD: "DD ars r (τ,σ,σ',τ')" and "set (labels τ) ⊆ ds r {β}"
and "length (labels σ) ≤ 1" and "set (labels σ) ⊆ {α}"
shows "∃σ1 σ2 σ3. (σ'=(fst σ1,snd σ1@snd σ2@snd σ3) ∧ lst σ1=fst σ2 ∧ lst σ2 = fst σ3 ∧ lst σ3 = lst σ'
                 ∧ LD_1' r β α (labels σ1) (labels σ2) (labels σ3))"
      "set (labels τ') ⊆ ds r ({α,β})"
proof -
 show "∃ σ1 σ2 σ3. (σ' = (fst σ1,snd σ1@snd σ2@snd σ3) ∧
         lst σ1 = fst σ2 ∧ lst σ2 = fst σ3 ∧ lst σ3 = lst σ' ∧ LD_1' r β α (labels σ1) (labels σ2) (labels σ3))" proof -
 from DD have σ':"σ' ∈ seq ars" using assms unfolding DD_def diagram_def by auto
 from DD have x: "(r|labels σ'| -s dl r (labels τ),r|labels σ| ) ∈ mul_eq r" unfolding DD_def D2_def using D_eq(2)[OF t i] by auto
  have "dl r (labels τ) ⊆ ds r (ds r {β})" using assms(4) unfolding dl_def ds_def by auto
  hence "dl r (labels τ) ⊆ ds r {β}" using ds_ds_subseteq_ds[OF t] by auto
  hence x:"(r|labels σ'| -s ds r {β},r|labels σ| ) ∈ mul_eq r" using x unfolding diff_def by (metis diff_def lemma2_6_8 mul_eq_trans t)
  hence x:"(r|labels σ'| -s dl r [β],{#α#}) ∈ mul_eq r" using labels_multiset[OF assms(5,6)] unfolding dl_def using mul_eq_trans[OF t x] by auto
  obtain σ1' σ2' σ3' where l:"labels σ' = σ1'@(σ2'@σ3')" and σ1'l: "set σ1' ⊆ ds r {β}" and
   σ2'l: "length σ2' ≤ 1 ∧ set σ2' ⊆ {α}" and σ3'l: "set σ3' ⊆ ds r {α,β}" using proposition3_4_inv_lists[OF t i x] unfolding dl_def by auto
  obtain σ1 σ23 where σ1:"σ1 ∈ seq ars" and σ23: "σ23 ∈ seq ars" and lf1: "lst σ1 = fst σ23" and lf1b: "lst σ' = lst σ23" and
   σ'_eq:"σ' = (fst σ1,snd σ1@snd σ23)" and σ1l:"labels σ1 = σ1'" and l2:"labels σ23 = σ2'@σ3'"
   using seq_decompose[OF σ' l] by auto
  obtain σ2 σ3 where σ2:"σ2 ∈ seq ars" and σ3:"σ3 ∈ seq ars" and lf2:"lst σ2 = fst σ3" and lf2b:"lst σ23 = lst σ3" and
   σ23_eq:"σ23 = (fst σ2,snd σ2@snd σ3)" and σ2l: "labels σ2 = σ2'" and σ3l: "labels σ3 = σ3'"
   using seq_decompose[OF σ23 l2] by auto
  have "σ' = (fst σ1, snd σ1 @ snd σ2 @ snd σ3)" using σ1 σ2 σ3 σ'_eq σ23_eq by auto
  moreover have "lst σ1 = fst σ2" using lf1 σ23_eq by auto
  moreover have "lst σ2 = fst σ3" using lf2 by auto
  moreover have "lst σ3 = lst σ'" using lf1b lf2b by auto
  moreover have "set (labels σ1) ⊆ ds r {β}" using σ1l σ1'l by auto
  moreover have "length (labels σ2) ≤ 1 ∧ set (labels σ2) ⊆ {α}" using σ2l σ2'l by auto
  moreover have "set (labels σ3) ⊆ ds r {α, β}" using σ3l σ3'l by auto
  ultimately show ?thesis unfolding LD_1'_def by fast
 qed
 show "set (labels τ') ⊆ ds r ({α,β})" proof -
  have x:"(r|labels τ'| -s dl r (labels σ),r|labels τ| ) ∈ mul_eq r" using DD D_eq[OF t i] unfolding DD_def D2_def by auto
  have y:"set_mset r|labels τ| ⊆ ds r {β}" using leq_imp_subseteq[OF lexmax_le_multiset[OF t]] assms(4) by auto
  hence  "set_mset (r|labels τ'|-s ds r (set (labels σ))) ⊆ ds r {β}" using mul_eq_and_ds_imp_ds[OF t x y] unfolding dl_def by auto
  hence "set_mset (r|labels τ'| ) ⊆ ds r {β} ∪ ds r (set (labels σ))" unfolding diff_def by auto
  hence "set_mset (r|labels τ'| ) ⊆ ds r {α,β}" using assms(6) unfolding ds_def by auto
  thus ?thesis using lexmax_set[OF t] by auto
 qed
qed

lemma local_decreasing_extended_imp_decreasing:
assumes "LT1 ars r (s,[β_step]) (s,[α_step]) γ1 γ2 γ3"
and t: "trans r" and i: "irrefl r"
and IH:"!!y . ((y,((s,[β_step]@υ_step),(s,[α_step]@ρ_step))) ∈ pex r ⟹ peak ars y ⟹ ∃σ' τ'. DD ars r (fst y, snd y, σ', τ'))" (is "!!y. ((y,?P) ∈ _ ⟹ _ ⟹ _)")
shows "∃ σ1 σ2 σ3' γ1'''. ({σ1,σ2,σ3',γ1'''} ⊆ seq ars ∧
  set (labels σ1) ⊆ ds r {fst β_step} ∧ length (labels σ2) ≤ 1 ∧ set (labels σ2) ⊆ {fst α_step} ∧ set (labels σ3') ⊆ ds r {fst α_step,fst β_step}) ∧
  set (labels γ1''') ⊆ ds r {fst α_step,fst β_step} ∧
  snd β_step = fst σ1 ∧ lst σ1 = fst σ2 ∧ lst σ2 = fst σ3' ∧ lst σ3' = lst γ1''' ∧ fst γ1''' = fst γ3"
proof -
 from assms labels_multiset have s2:"(r|labels γ2|,{#fst α_step#}) ∈ mul_eq r" unfolding LT1_def local_triangle1_def LD_1'_def labels_def by auto
 from assms have γ1: "γ1 ∈ conv ars" and γ3: "γ3 ∈ conv ars" and γ2_l: "length (labels γ2) ≤ 1"
  and γ2_s: "set (labels γ2) ⊆ {fst α_step}" and γ3_s: "set (labels_conv γ3) ⊆ ds r {fst α_step,fst β_step}"
  and "set (labels_conv γ1) ⊆ ds r {fst β_step}" unfolding LT_def LD'_def LT1_def LD_1'_def labels_def local_triangle1_def by auto
 hence "set_mset (measure_conv r γ1) ⊆ ds r {fst β_step}" unfolding measure_conv_def using lexmax_le_multiset[OF t] by (metis set_mset_mset submultiset_implies_subset subset_trans)
 hence γ1_s: "set_mset (measure_conv r γ1) ⊆ dm r {#fst β_step#}" unfolding dm_def by auto
 have x: "({#fst β_step#}, {#fst β_step, fst α_step#}) ∈ mul_eq r" using mul_eq_add_right[of "{#_#}"] by auto
 obtain γ1' γ1'' where γ1': "γ1' ∈ seq ars" and γ1'': "γ1'' ∈ seq ars" and eqx:"fst γ1' = fst γ1"
  and  "fst γ1'' = lst_conv γ1" and γ1'_eq: "lst γ1' = lst γ1''"  and m2: "set_mset (measure r (γ1',γ1'')) ⊆ dm r {#fst β_step#}"
  using conv_imp_valley[OF t IH γ1 γ1_s x] apply auto by fast
 hence Q:"peak ars (γ1'',γ2)" (is "peak ars ?Q") unfolding peak_def using assms(1) unfolding LT_def LD'_def LT1_def local_triangle1_def by auto
 from m2 have  γ1's: "set (labels γ1') ⊆ ds r {fst β_step}" and γ1''s: "set (labels γ1'') ⊆ ds r {fst β_step}" unfolding measure_def dm_def using lexmax_set[OF t] by auto
 from m2 have τ1'_m:"(r|labels γ1''|,{#fst β_step#}) ∈ mul r" unfolding measure_def mul_def apply auto by (metis dm_def empty_neutral(1) set_mset_single add_mset_not_empty)
 hence y:"(r|labels γ1''| + r|labels γ2|,{#fst α_step#}+{#fst β_step#}) ∈ mul r" using mul_add_mul_eq_imp_mul[OF τ1'_m s2] union_commute by metis
 have "(r|labels γ1''| + r|labels γ2|, {#fst α_step,fst β_step#} + (r|map fst ρ_step|-sds r {fst α_step} + r|map fst υ_step|-sds r {fst β_step})) ∈ mul r" using mul_add_right[OF y] by (auto simp: add_mset_commute)
 hence q:"(?Q,?P) ∈ pex r"  unfolding pex_def measure_def labels_def apply auto by (metis union_assoc union_commute union_lcomm)
 obtain γ1''' σ' where DD:"DD ars r (γ1'',γ2,σ',γ1''')" using IH[OF q Q] by auto
 from DD have σ': "σ' ∈ seq ars" and γ1''':"γ1''' ∈ seq ars" unfolding DD_def diagram_def by auto
 from decreasing_imp_local_decreasing[OF t i DD γ1''s γ2_l γ2_s] obtain σ1' σ2' σ3' where σ'_dec: "σ' = (fst σ1', snd σ1' @ snd σ2' @ snd σ3')"
   and eq1: "lst σ1' = fst σ2'" "lst σ2' = fst σ3'" "lst σ3' = lst σ'"
   and σ1s: "set (labels σ1') ⊆ ds r {fst β_step}" and σ2l: "length (labels σ2') ≤ 1" and σ2's: "set (labels σ2') ⊆ {fst α_step}" and "set (labels σ3') ⊆ ds r {fst α_step,fst β_step}"
   and σ3's: "set (labels σ3') ⊆ ds r {fst α_step,fst β_step}" and γ1'''s: "set (labels γ1''') ⊆ ds r {fst α_step,fst β_step}" unfolding LD_1'_def by blast
 have σ'_ds: "(fst σ1', snd σ1' @ snd σ2' @ snd σ3') ∈ seq ars" using σ' σ'_dec by auto
 have σ1':"σ1' ∈ seq ars" and tmp: "(fst σ2',snd σ2'@snd σ3') ∈ seq ars" using seq_chop[OF σ'_ds] surjective_pairing eq1 by auto
 have σ2': "σ2' ∈ seq ars" and σ3': "σ3' ∈ seq ars" using seq_chop[OF tmp] using surjective_pairing eq1 by auto
 have eq:"lst γ1' = fst σ1'" using DD γ1'_eq unfolding DD_def diagram_def apply auto unfolding σ'_dec by auto
 have σ1: "(fst γ1',snd γ1'@snd σ1') ∈ seq ars" (is "?σ1 ∈ _") and eq0:"lst (fst γ1', snd γ1' @ snd σ1') = lst σ1'" using seq_concat[OF γ1' σ1' eq] by auto
 moreover have "set (labels ?σ1) ⊆ ds r {fst β_step}" using σ1s γ1's unfolding labels_def dm_def by auto
 moreover have "snd β_step = fst ?σ1" using assms(1) unfolding LT1_def local_triangle1_def lst_def σ'_dec eqx by auto
 moreover have "lst ?σ1 = fst σ2'" unfolding eq0 eq1 by auto
 moreover have "lst σ3' = lst γ1'''" unfolding eq1 using DD unfolding DD_def diagram_def by auto
 moreover have "fst γ1''' = fst γ3" using DD assms(1) unfolding DD_def diagram_def LT1_def local_triangle1_def by auto
 ultimately show ?thesis using σ2' σ2's σ3' σ3's  γ1''' γ1'''s eq1 surjective_pairing σ2l by blast
qed

lemma LDD_imp_DD:
assumes t:"trans r" and i:"irrefl r" and "LDD ars r (τ,σ,σ1,σ2,σ3,τ1,τ2,τ3)"
shows "∃ σ' τ'. DD ars r (τ,σ,σ',τ')" proof -
 from assms have "length (labels σ) = 1"  unfolding LDD_def LDD1_def local_diagram1_def local_peak_def unfolding labels_def by auto
 from this obtain α where l: "labels σ = [α]" by (metis append_Nil append_butlast_last_id butlast_conv_take diff_self_eq_0 length_0_conv take_0 zero_neq_one)
 hence σl: "labels σ = [hd (labels σ)]" by auto
 from assms have "length (labels τ) = 1"  unfolding LDD_def LDD1_def local_diagram1_def local_peak_def unfolding labels_def by auto
 from this obtain β where l: "labels τ = [β]" by (metis append_Nil append_butlast_last_id butlast_conv_take diff_self_eq_0 length_0_conv take_0 zero_neq_one)
 hence τl: "labels τ = [hd (labels τ)]" by auto
 from assms have σ':"(fst σ1,snd σ1@snd σ2@snd σ3) ∈ seq ars" (is "?σ' ∈ _") and τ':"(fst τ1,snd τ1@snd τ2@snd τ3) ∈ seq ars" (is "?τ' ∈ _")
  unfolding LDD_def LDD1_def local_diagram1_def local_peak_def peak_def apply auto apply (metis fst_eqD seq_concat(1) snd_eqD)  by (metis fst_eqD seq_concat(1) snd_eqD)
 from assms have sigmas: "fst ?σ' = fst σ1" "lst ?σ' = lst σ3" unfolding LDD_def LDD1_def local_diagram1_def local_peak_def peak_def apply auto by (metis (opaque_lifting, no_types) σ' append_assoc seq_chop(1) seq_concat(2) seq_concat_helper)
 from assms have taus: "fst ?τ' = fst τ1" "lst ?τ' = lst τ3" unfolding LDD_def LDD1_def local_diagram1_def local_peak_def peak_def apply auto  by (metis (opaque_lifting, no_types) τ' append_assoc seq_chop(1) seq_concat(2) seq_concat_helper)
 have "diagram ars (τ,σ,?σ',?τ')" using assms unfolding LDD_def LDD1_def local_diagram1_def diagram_def local_peak_def apply auto
  unfolding peak_def apply auto using sigmas taus σ' τ' by auto
 moreover have "D2 r (τ,σ,?σ',?τ')" using assms proposition3_4[OF t i] σl τl unfolding LDD_def LDD1_def D2_def LD'_def labels_def by auto
 ultimately show ?thesis unfolding DD_def by auto
qed

lemma LT_imp_DD:
assumes t:"trans r"
and i:"irrefl r"
and IH:"!!y . ((y,((s,[β_step]@υ_step),(s,[α_step]@ρ_step))) ∈ pex r ⟹ peak ars y ⟹ ∃σ' τ'. DD ars r (fst y, snd y, σ', τ'))" (is "!!y. ((y,?P) ∈ _ ⟹ _ ⟹ _)")
and LT: "LT ars r ((s,[β_step]),(s,[α_step]),γ1,γ2,γ3,δ1,δ2,δ3)"
shows "∃ κ μ. DD ars r ((s,[β_step]),(s,[α_step]),κ,μ)"
proof -
    from LT have LTa: "LT1 ars r (s,[β_step]) (s,[α_step]) γ1 γ2 γ3" and LTb: "LT1 ars r (s,[α_step]) (s,[β_step]) δ1 δ2 δ3" unfolding LT_def by auto

    from local_decreasing_extended_imp_decreasing[OF LTa t i IH] obtain σ1 σ2 σ3' γ1''' where sigmas:"{σ1,σ2,σ3',γ1'''} ⊆ seq ars" and
    onetwo1: "set (labels σ1) ⊆ ds r {fst β_step} ∧ length (labels σ2) ≤ 1 ∧ set (labels σ2) ⊆ {fst α_step} ∧
    set (labels σ3') ⊆ ds r {fst α_step, fst β_step} ∧ set (labels γ1''') ⊆ ds r {fst α_step,fst β_step} ∧
     snd β_step = fst σ1 ∧ lst σ1 = fst σ2 ∧ lst σ2 = fst σ3' ∧ lst σ3' = lst γ1''' ∧ fst γ1''' = fst γ3" by metis

    have ih2: "!!y. (y, (s, [α_step] @ ρ_step),(s,[β_step] @ υ_step)) ∈ pex r ⟹ peak ars y ⟹ ∃σ' τ'. DD ars r (fst y, snd y, σ', τ')"
    using IH unfolding pex_def measure_def by (auto simp: union_commute)

    from local_decreasing_extended_imp_decreasing[OF LTb t i ih2] obtain τ1 τ2 τ3' δ1''' where taus:"{τ1,τ2,τ3',δ1'''} ⊆ seq ars" and
    onetwo2: "set (labels τ1) ⊆ ds r {fst α_step} ∧ length (labels τ2) ≤ 1 ∧ set (labels τ2) ⊆ {fst β_step} ∧
    set (labels τ3') ⊆ ds r {fst β_step,fst α_step} ∧ set (labels δ1''') ⊆ ds r {fst β_step,fst α_step} ∧
     snd α_step = fst τ1 ∧ lst τ1 = fst τ2 ∧ lst τ2 = fst τ3' ∧ lst τ3' = lst δ1''' ∧ fst δ1''' = fst δ3" by metis

    have γ3: "γ3 ∈ conv ars" and γ3m:"set (labels_conv γ3) ⊆ ds r {fst α_step,fst β_step}" and
         δ3: "δ3 ∈ conv ars" (is "?c2 ∈ _") and δ3m: "set (labels_conv δ3) ⊆ ds r {fst β_step,fst α_step}" and
         eq: "lst_conv γ3 = lst_conv δ3" using LT unfolding LT_def LT1_def local_triangle1_def LD_1'_def labels_def by auto
    hence δ3m: "set (labels_conv δ3) ⊆ ds r {fst α_step, fst β_step}" using insert_commute by metis

    (*concat*)
    have δ1''': "δ1''' ∈ seq ars" using taus by auto
    have γ1''': "γ1''' ∈ seq ars" using sigmas by auto
    have c1: "(fst δ1''',map (Pair True) (snd δ1''')) ∈ conv ars" (is "?c0 ∈ _")
      using seq_imp_conv δ1''' surjective_pairing by metis
    have c11: "lst δ1''' = lst_conv ?c0" using seq_imp_conv δ1''' surjective_pairing by metis
    have c1l: "set (labels_conv ?c0) ⊆ ds r {fst β_step,fst α_step}" using onetwo2 seq_imp_conv δ1''' surjective_pairing by metis
    hence c1l:"set (labels_conv ?c0) ⊆ ds r {fst α_step,fst β_step}" using insert_commute by metis

    have c1: "conv_mirror ?c0 ∈ conv ars" (is "?c1 ∈ _")
             "set (labels_conv (conv_mirror ?c0)) ⊆ ds r {fst α_step,fst β_step}"
             "fst (conv_mirror ?c0) = lst τ3'"
             "lst_conv (conv_mirror ?c0) = fst δ3"
     using conv_mirror[OF c1] c11 c1l c1 onetwo2 by auto


    have c2: "?c2 ∈ conv ars"
             "set (labels_conv ?c2) ⊆ ds r {fst α_step, fst β_step}"
             "fst ?c2 = fst δ3"
             "lst_conv ?c2 = lst_conv γ3" using δ3 eq δ3m by auto

    have "conv_mirror γ3 ∈ conv ars" (is "?c3 ∈ _") "set (labels_conv (conv_mirror γ3)) = set (labels_conv γ3)" using conv_mirror[OF γ3] by auto
    hence c3: "?c3 ∈ conv ars"
              "set (labels_conv ?c3) ⊆ ds r {fst α_step, fst β_step}"
              "fst ?c3 = lst_conv δ3"
              "lst_conv ?c3 = fst γ1'''" using conv_mirror[OF γ3] eq onetwo1 γ3m by auto

    have c4: "(fst γ1''',map (Pair True) (snd γ1''')) ∈ conv ars" (is "?c4 ∈ _") "set (labels_conv (fst γ1''',map (Pair True) (snd γ1'''))) = set (labels γ1''')"
     using seq_imp_conv γ1''' surjective_pairing apply metis using seq_imp_conv γ1''' surjective_pairing by metis
    have c4: "?c4 ∈ conv ars"
             "lst_conv ?c4 = lst γ1'''"
             "set (labels_conv ?c4) ⊆ ds r {fst α_step,fst β_step}"
     using  seq_imp_conv γ1''' surjective_pairing apply metis using seq_imp_conv γ1''' surjective_pairing apply metis using c4(2) onetwo1 by auto

    have eq: "lst_conv ?c1 = fst ?c2" using c1 c2 by auto
    have c12: "(fst ?c1,snd ?c1@snd ?c2) ∈ conv ars" (is "?c12 ∈ _")
     "fst (fst ?c1,snd ?c1@snd ?c2) = fst ?c1" "lst_conv (fst ?c1,snd ?c1@snd ?c2) = lst_conv ?c2" using conv_concat[OF c1(1) c2(1) eq] by auto
    have eq: "lst_conv ?c12 = fst ?c3" using c12 c3 by auto
    have c123: "(fst ?c12,snd ?c12@snd ?c3) ∈ conv ars" (is "?c123 ∈ _")
     "fst (fst ?c12,snd ?c12@snd ?c3) = fst ?c12" "lst_conv (fst ?c12,snd ?c12@snd ?c3) = lst_conv ?c3" using conv_concat[OF c12(1) c3(1) eq] by auto

    have eq: "lst_conv ?c123 = fst ?c4" using c123 c2 c4 onetwo1 onetwo2 apply auto unfolding Let_def using c3(4) apply auto by metis
    have c1234: "(fst ?c123,snd ?c123@snd ?c4) ∈ conv ars" (is "?c1234 ∈ _")
     "fst (fst ?c123,snd ?c123@snd ?c4) = fst ?c123" "lst_conv (fst ?c123,snd ?c123@snd ?c4) = lst_conv ?c4" using conv_concat[OF c123(1) c4(1) eq] by auto
    hence c1234: "?c1234 ∈ conv ars" (is "?c1234 ∈ _")
     "fst (?c1234) = lst τ3'" "lst_conv ?c1234 = lst σ3'" apply auto unfolding Let_def using c1(3) apply auto apply metis using c4(2) onetwo1 by metis

    have c12l: "set (labels_conv ?c12) ⊆ ds r {fst α_step, fst β_step}" using conv_concat_labels[OF c1(1) c2(1)] c1 c2 by auto
    have c123l: "set (labels_conv ?c123) ⊆ ds r {fst α_step,fst β_step}" using conv_concat_labels[OF c12(1) c3(1)] c12l c3 by auto
    have c1234l:"set (labels_conv ?c1234) ⊆ ds r {fst α_step,fst β_step}" using conv_concat_labels[OF c123(1) c4(1)] c123l c4 by auto
    hence "set_mset (r|labels_conv ?c1234| ) ⊆ ds r {fst α_step,fst β_step}" using submultiset_implies_subset[OF lexmax_le_multiset[OF t]] by auto
    hence "set_mset (measure_conv r ?c1234) ⊆ dm r {#fst β_step, fst α_step#}" unfolding measure_conv_def dm_def by (auto simp: add_mset_commute)
    hence m: "set_mset (measure_conv r ?c1234) ⊆ dm r {#fst α_step, fst β_step#}" by (auto simp: add_mset_commute)

    from c1234 m obtain ρ where ρ:"ρ ∈ conv ars" and ρm:"set_mset (measure_conv r ρ) ⊆ dm r {# fst α_step, fst β_step#}"
    and eq1: "fst ρ = lst τ3'" and eq2: "lst_conv ρ = lst σ3'" by auto

    have M:"({#fst α_step,fst β_step#},{#fst β_step,fst α_step#}) ∈ mul_eq r" using mul_eq_reflexive add_mset_commute by metis
    from conv_imp_valley[OF t IH ρ ρm M] obtain τ3'' σ3'' where
     τ3'':"τ3'' ∈ seq ars" and σ3'': "σ3'' ∈ seq ars" and eq:"fst τ3'' = fst ρ ∧ fst σ3'' = lst_conv ρ ∧ lst τ3'' = lst σ3'' ∧
    set_mset (measure r (τ3'', σ3'')) ⊆ dm r {#fst α_step, fst β_step#}"  apply auto by fast
    have s1: "set (labels σ3'') ⊆ ds r {fst α_step, fst β_step}" using eq unfolding dm_def measure_def apply auto by (metis (opaque_lifting, no_types) insert_commute lexmax_set subsetD t)
    have s2: "set (labels τ3'') ⊆ ds r {fst β_step, fst α_step}" using eq unfolding dm_def measure_def apply auto by (metis (opaque_lifting, no_types) insert_commute lexmax_set subsetD t)
    have σ1_eq: "lst (s, [β_step]) = fst σ1" and τ1_eq: "lst (s, [α_step]) = fst τ1" using onetwo1 onetwo2 surjective_pairing unfolding lst_def by auto
    have eqn: " lst τ3'' = lst σ3''" and σ_eq: "lst σ3' = fst σ3''" and τ_eq: "lst τ3' = fst τ3''" using eq eq1 eq2 by auto
    have σ3':"(fst σ3',snd σ3'@snd σ3'') ∈ seq ars" (is "?σ3 ∈ _") using seq_concat[OF _ σ3'' σ_eq] sigmas by blast
    have τ3':"(fst τ3',snd τ3'@snd τ3'') ∈ seq ars" (is "?τ3 ∈ _") using seq_concat[OF _ τ3'' τ_eq] taus by blast
    have "fst ?σ3 = lst σ2" and "fst ?τ3 = lst τ2" using onetwo1 onetwo2 by auto
    have lst:"lst ?σ3 = lst ?τ3" using eqn σ3'' σ3' σ_eq τ3'' τ_eq τ3' seq_chop(1) seq_concat(2) surjective_pairing by metis
    have "local_diagram1 ars (s, [β_step]) (s, [α_step]) σ1 σ2 (fst σ3', snd σ3' @ snd σ3'')"
     using sigmas σ3' onetwo1 σ1_eq LT unfolding local_diagram1_def  LT_def LT1_def local_triangle1_def by auto
    moreover have "local_diagram1 ars (s,[α_step]) (s,[β_step]) τ1 τ2 (fst τ3',snd τ3'@snd τ3'')"
     using taus τ3' onetwo2 τ1_eq LT unfolding local_diagram1_def LT_def LT1_def local_triangle1_def by auto
    moreover have "LD_1' r (hd (labels (s, [β_step]))) (hd (labels (s, [α_step]))) (labels σ1) (labels σ2) (labels (fst σ3', snd σ3' @ snd σ3''))"
     using onetwo1 s1 unfolding LD_1'_def labels_def by auto
    moreover have "LD_1' r (hd (labels (s, [α_step]))) (hd (labels (s, [β_step]))) (labels τ1) (labels τ2) (labels (fst τ3', snd τ3' @ snd τ3''))"
     using onetwo2 s2 unfolding LD_1'_def labels_def by auto
    ultimately have LDD: "LDD ars r ((s,[β_step]),(s,[α_step]),σ1,σ2,?σ3,τ1,τ2,?τ3)" using lst unfolding LDD_def LDD1_def local_diagram1_def by auto
    from LDD_imp_DD[OF t i LDD] show ?thesis by auto
qed

lemma LT_imp_D: assumes t:"trans r" and "wf r" and "∀p. (local_peak ars p ⟶ (∃ γ1 γ2 γ3 δ1 δ2 δ3. LT ars r (fst p,snd p,γ1,γ2,γ3,δ1,δ2,δ3)))"
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
    hence alpha': "(s,fst α_step, snd α_step) ∈ ars" by (metis seq_tail1(2))
    have beta:"(s,[β_step]) ∈ seq ars" (is "?β ∈ _")
     and upsilon: "(lst (s,[β_step]),υ_step) ∈ seq ars" (is "?υ ∈ _") using seq_chop[OF tau2] by auto

    have lp:"local_peak ars (?β,?α)" using alpha beta unfolding local_peak_def peak_def by auto

   (* difference begin*)
    from this obtain γ1 γ2 γ3 δ1 δ2 δ3 where LT: "LT ars r (?β, ?α, γ1, γ2, γ3, δ1, δ2, δ3)" using assms(3) apply auto by metis
    have P:"P = ((s,[β_step]@υ_step),(s,[α_step]@ρ_step))" (is "P = ?P") using decompose unfolding tau_dec sigma_dec by auto
    obtain κ μ where D:"DD ars r (?β,?α,κ,μ)" using LT_imp_DD[OF t i 1(1) LT] unfolding P by fast
   (*difference end*)

    hence kappa: "κ∈seq ars" and mu: "μ∈seq ars" unfolding DD_def diagram_def by auto
    have P_IH1: " peak ars (?υ,κ)" using upsilon kappa D unfolding DD_def diagram_def peak_def by auto
    have beta_ne: "labels ?β ≠ []" unfolding labels_def by auto
    have dec: "D r (labels ?β) (labels ?α) (labels κ) (labels μ)" using D unfolding DD_def D2_def by auto
    have x1:"((?υ,κ), (τ,?α)) ∈ pex r" using lemma3_6[OF assms(1) beta_ne dec]
     unfolding pex_def measure_def decompose labels_def tau_dec apply (auto simp: add_mset_commute) using union_commute by metis
    have "(lexmax r (labels τ) + lexmax r (labels (?α)), lexmax r (labels τ) + lexmax r (labels σ)) ∈ mul_eq r" (is "(?l,?r) ∈ _")
      unfolding sigma_dec labels_def snd_conv list.map lexmax.simps diff_from_empty by (simp add: lemma2_6_2_a t)
    hence "((?υ,κ),P) ∈ pex r" using x1 unfolding sigma_s pex_def measure_def decompose using mul_and_mul_eq_imp_mul[OF assms(1)] by auto
    from this obtain κ' υ' where IH1: "DD ars r (?υ,κ,κ',υ')" using 1(1)[OF _ P_IH1] unfolding decompose by auto
    hence kappa':"κ'∈seq ars" and upsilon': "υ'∈seq ars" using D unfolding DD_def diagram_def by auto
    have tau': "(fst μ,snd μ@(snd υ')) ∈ seq ars" (is "?τ' ∈ _") using seq_concat(1)[OF mu upsilon'] D IH1 unfolding DD_def diagram_def by auto
    have DIH1: "DD ars r (τ,?α,κ',?τ')" using lemma3_5_DD[OF assms(1) i D IH1] tau_dec by auto
    hence dec_dih1: "D r (labels τ) (labels ?α) (labels κ') (labels ?τ')" using DIH1 unfolding DD_def D2_def by simp

    have P_IH2: "peak ars (?τ',?ρ)" using tau' rho D unfolding DD_def diagram_def peak_def by auto
    have alpha_ne: "labels ?α ≠ []" unfolding labels_def by simp
    have "((?τ',?ρ),P) ∈ pex r" using lemma3_6_v[OF assms(1) i alpha_ne dec_dih1] unfolding pex_def measure_def decompose labels_def sigma_dec by auto
    from this obtain ρ' τ'' where IH2: "DD ars r (?τ',?ρ,ρ',τ'')" using 1(1)[OF _ P_IH2] by auto
    show ?thesis using lemma3_5_DD_v[OF assms(1) i DIH1 IH2] unfolding decompose fst_conv snd_conv sigma_dec by fast
   qed
  qed
 qed
qed

definition LD_conv :: "'b set ⇒ 'a rel ⇒ bool"
 where "LD_conv L ars = (∃ (r:: ('b rel)) (lrs::('a,'b) lars). (ars = unlabel lrs) ∧ trans r ∧ wf r ∧ (∀p. (local_peak lrs p ⟶ (∃ γ1 γ2 γ3 δ1 δ2 δ3. LT lrs r (fst p,snd p,γ1,γ2,γ3,δ1,δ2,δ3)))))"

lemma sound_conv: assumes "LD_conv L ars" shows "CR ars"
 using assms LT_imp_D D_imp_CR unfolding LD_conv_def by metis

hide_const (open) D
hide_const (open) seq
hide_const (open) measure

hide_fact (open) split

end