theory Decreasing_Diagrams imports Multiset Abstract_Rewriting begin
  
(*Appendix*)
definition diff :: "'a multiset \<Rightarrow> 'a set \<Rightarrow> 'a multiset" ("(_-s_)" [999] 998)
 where "M -s S = Multiset.filter (\<lambda>x. x \<notin> S) M"

definition intersect :: "'a multiset \<Rightarrow> 'a set \<Rightarrow> 'a multiset" ("(_\<inter>s_)" [999] 998)
 where "M \<inter>s S = Multiset.filter (\<lambda>x. x \<in> S) M"

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 \<le> N" shows "set_of M \<subseteq> set_of N" 
 using assms mset_leD by auto 

lemma subset_implies_remove_empty: assumes "set_of M \<subseteq> 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_of M \<subseteq> S" proof
 fix x assume A: "x \<in> set_of M" 
 have "x \<notin> set_of (M -s S)" using assms by auto
 thus "x \<in> 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 \<union> T)" unfolding diff_def by (rule multiset_eqI) simp
lemma lemmaA_3_10: "M = (M \<inter>s S) + (M -s S)" using multiset_partition unfolding diff_def intersect_def filter_def by auto
lemma lemmaA_3_11: "(M -s T) \<inter>s S = (M \<inter>s S) -s T" unfolding diff_def intersect_def by (rule multiset_eqI) simp

(*Definition 2.5(1)*)
definition ds :: "'a rel \<Rightarrow> 'a set \<Rightarrow> 'a set"
 where "ds r S = {y . \<exists>x \<in> S. (y,x) \<in> r}"

definition dm :: "'a rel \<Rightarrow> 'a multiset \<Rightarrow> 'a set" 
 where "dm r M = ds r (set_of M)"

definition dl :: "'a rel \<Rightarrow> 'a list \<Rightarrow> 'a set" 
 where "dl r \<sigma> = ds r (set \<sigma>)"

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

(*Definition 2.5(2)*)

(*strict order (mult) is used from Multiset.thy*)
definition mult_eq :: "'a rel \<Rightarrow> 'a multiset rel" where
  "mult_eq r = (mult1 r)\<^sup>*"

definition mul :: "'a rel \<Rightarrow> 'a multiset rel" where
  "mul r = {(M,N).\<exists>I J K. M = I + K \<and> N = I + J \<and> set_of K \<subseteq> dm r J \<and> J \<noteq> {#}}"

definition mul_eq :: "'a rel \<Rightarrow> 'a multiset rel" where
  "mul_eq r = {(M,N).\<exists>I J K. M = I + K \<and> N = I + J \<and> set_of K \<subseteq> dm r J}"

lemma downset_intro: 
assumes "\<forall>k\<in>set_of K.\<exists>j\<in>set_of J.(k,j)\<in>r" shows "set_of K \<subseteq> dm r J" proof
 fix x assume "x\<in>set_of K" thus "x \<in> dm r J" using assms unfolding dm_def ds_def by fast
qed

lemma downset_elim:
assumes "set_of K \<subseteq> dm r J" shows "\<forall>k\<in>set_of K.\<exists>j\<in>set_of J.(k,j)\<in>r" proof
 fix k assume "k\<in> set_of K" thus "\<exists>j\<in>set_of J.(k,j)\<in> 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) \<in> mult_eq r" shows "\<exists>I J K. N = I + J \<and> M = I + K \<and> set_of K \<subseteq> dm r J" 
proof (cases "(M,N) \<in> 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 + {#} \<and> M = M + {#} \<and> set_of {#} \<subseteq> 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_of K \<subseteq> dm r J" shows "(I+K,I+J)\<in>mult_eq r"
proof (cases "set_of J = {}")
 case True hence "set_of 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 \<noteq> {#}" using set_of_eq_empty_iff by auto
  hence "(I+K,I+J)\<in> mult r" using set_of_eq_empty_iff assms one_step_implies_mult downset_elim by fast 
  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 \<subseteq> mul r" proof
  fix N M assume A: "(N,M) \<in> mult r" show "(N,M) \<in> mul r" proof -
   obtain I J K where "M = I + J" and "N = I + K" and "J \<noteq> {#}" and "set_of K \<subseteq> 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 \<subseteq> mult r" proof
  fix N M assume A: "(N,M) \<in> mul r" show "(N,M) \<in> mult r" proof -
   obtain I J K where "M = I + J" and "N = I + K" and "J \<noteq> {#}" and "set_of K \<subseteq> 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 \<subseteq> mul_eq r" proof 
  fix N M assume A: "(N,M) \<in> mult_eq r" show "(N,M) \<in> mul_eq r" proof (cases "(N,M) \<in> 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 + {#} \<and> N = N + {#} \<and> set_of {#} \<subseteq> dm r {#}" by auto
   thus ?thesis unfolding eq unfolding mul_eq_def by fast
  qed
 qed
 show "mul_eq r \<subseteq> mult_eq r" using one_step_implies_mult_eq[OF assms] unfolding mul_eq_def by auto
qed

lemma "mul_eq r = (mul r)\<^sup>=" proof
 show "mul_eq r \<subseteq> (mul r)\<^sup>=" proof
  fix M N assume A:"(M,N) \<in> mul_eq r" show "(M,N) \<in> (mul r)\<^sup>=" proof -
   from A obtain I J K where 1: "M = I + K" and 2: "N = I + J" and 3: "set_of K \<subseteq> 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 \<supseteq> (mul r)\<^sup>=" proof 
  fix M N assume A:"(M,N) \<in> (mul r)\<^sup>=" show "(M,N) \<in> mul_eq r"
   proof (cases "M = N")
    case True hence "M = M + {#}" and "N = M + {#}" and "set_of {#} \<subseteq> dm r {#}" by auto
    thus ?thesis unfolding mul_eq_def by fast
   next
    case False hence "(M,N) \<in> mul r" using A by auto
    thus ?thesis unfolding mul_def mul_eq_def by auto
  qed
 qed
qed

(* useful properties on multisets *)
lemma mul_eq_reflexive: "(M,M) \<in> mul_eq r" proof -
 have "M = M + {#}" and "set_of {#} \<subseteq> dm r {#}" by auto
 thus ?thesis unfolding mul_eq_def by fast
qed

lemma mul_eq_trans: assumes "trans r" and "(M,N) \<in> mul_eq r" and "(N,P) \<in> mul_eq r" shows "(M,P) \<in> 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, {#\<alpha>#}) \<in> mul_eq r" shows "M = {#\<alpha>#} \<or> set_of M \<subseteq> dm r {#\<alpha>#}" proof -
 from assms obtain I J K where 1:"M = I + K" and 2:"{#\<alpha>#} = I + J" and 3:"set_of K \<subseteq> dm r J" unfolding mul_eq_def by auto
 thus ?thesis proof (cases "I = {#}")
  case True hence "J = {#\<alpha>#}" using 2 by auto
  thus ?thesis using 1 3 True by auto
 next
  case False hence i: "I = {#\<alpha>#}" 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) \<in> mul r" and "(N,P) \<in> mul_eq r" shows "(M,P) \<in> 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 {#\<alpha>#} = {#}" shows "(M,{#\<alpha>#}) \<in> mul r" proof -
 from assms have C: "set_of M \<subseteq> dm r {#\<alpha>#}" by (metis remove_empty_implies_subset)
 have "M = {#}+M" and "{#\<alpha>#}={#}+{#\<alpha>#}" and "{#\<alpha>#} \<noteq> {#}" by auto
 thus ?thesis using C unfolding mul_def by fast
qed

(* Lemma 2.6 *)

lemma lemma2_6_1_set: "ds r (S \<union> T) = ds r S \<union> ds r T"
 unfolding set_of_union ds_def by auto 

lemma lemma2_6_1_list: "dl r (\<sigma>@\<tau>) = dl r \<sigma> \<union> dl r \<tau>" 
 unfolding dl_def ds_def set_append by auto

lemma lemma2_6_1_multiset: "dm r (M + N) = dm r M \<union> dm r N"
 unfolding dm_def set_of_union ds_def by auto 

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

text {* missing *}
lemma dl_monotone: "dl r (\<sigma>@\<tau>) \<subseteq> dl r (\<sigma>@\<tau>'@\<tau>)" unfolding lemma2_6_1_list by auto

(*Lemma 2.6.2*)

lemma lemma2_6_2_a: assumes t: "trans r" and "M \<le> N" shows "(M,N) \<in> mul_eq r" proof -
 from assms(2) obtain J where "N=M+J" by (metis assms(2) mset_le_exists_conv) 
 hence "M = M + {#}" and "N = M + J" and "set_of {#} \<subseteq> dm r J" by auto
 thus ?thesis unfolding mul_eq_def by fast
qed

lemma mul_eq_not_equal_imp_elt: 
assumes "(M,N)\<in>mul_eq r" and "y\<in>set_of M - set_of N" shows "\<exists>z\<in>set_of N.(y,z)\<in>r" proof - 
 from assms obtain I J K where "N=I+J" and "M=I+K" and F3:"set_of K \<subseteq> 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) \<in> mul_eq r" shows "dm r M \<subseteq> dm r N" proof
 fix x assume A: "x \<in> dm r M" show "x \<in> dm r N" proof -
  from A obtain y where F2:"y\<in>set_of M" and F3:"(x,y)\<in>r" unfolding dm_def ds_def by auto
  hence "\<exists> z \<in> set_of N. (x,z)\<in>r" proof (cases "y\<in>set_of 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

(*Lemma 2.6.3*)
lemma lemma2_6_3_step: 
assumes t:"trans r" and i:"irrefl r" and P:"set_of K \<subseteq> dm r J" shows "set_of (K-(J#\<inter>K)) \<subseteq> dm r (J-(J#\<inter>K))" proof  
 fix k assume K: "k \<in> set_of (K - (J#\<inter>K))" show "k \<in> dm r (J - (J#\<inter>K))" proof -
  have k: "k \<in># K" using K by simp
  have step: "k \<in> dm r (J-K)" proof -
   {
   fix K' have "K' \<le> K \<Longrightarrow> k \<in> dm r (J-K')" using k proof (induct K' arbitrary:k rule:multiset_induct)
    case empty thus ?case using P by auto
   next
    case (add Q q)
    have h1: "q \<in># K" and h2: "Q \<le> K" using mset_le_insertD[OF add(2)] by auto
    obtain j where mem1: "j\<in>set_of (J - Q)" and rel1: "(k, j) \<in> r" using add(1)[OF h2 add(3)] unfolding dm_def ds_def by auto
    show ?case proof (cases "j \<in># 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\<in>set_of (J - Q)" and rel2: "(j, j2) \<in> r" using eq add(1)[OF h2 h1] unfolding dm_def ds_def by auto
     have rel: "(k,j2) \<in> r" using transD[OF assms(1) rel1 rel2] by auto
     have "j2 \<noteq> 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 #\<inter> 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) \<in> mul_eq r" 
shows "\<exists> I J K. N = I + J \<and> M = I + K \<and> J#\<inter>K = {#} \<and> set_of K \<subseteq> 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_of K \<subseteq> dm r J" unfolding mul_eq_def by fast
 hence "N = (I + (J #\<inter> K)) + (J - (J #\<inter> K))"
  by (metis diff_union_cancelL inf_le2 multiset_diff_union_assoc multiset_inter_commute union_commute union_lcomm)
 moreover have "M = (I + (J #\<inter> K)) + (K - (J #\<inter> 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#\<inter>K)) #\<inter> (K-(J#\<inter>K)) = {#}" by (rule multiset_eqI) auto
 ultimately show ?thesis using lemma2_6_3_step[OF t i f3] by auto
qed 

(*Lemma 2.6.4*)
lemma lemma2_6_4: assumes t: "trans r" and "N \<noteq> {#}" and "set_of M \<subseteq> dm r N" shows "(M,N) \<in> 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 \<subseteq> S" and "(M,N) \<in> mul_eq r" 
shows "(M -s S, N -s S) \<in> 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_of K \<subseteq> dm r J" unfolding mul_eq_def by best
 from a b have A: "N-sS = (I-sS)+(J-sS)" and B: "M-sS = (I-sS)+(K-sS)" using lemmaA_3_8 by auto
 have C: "set_of (K-sS) \<subseteq> dm r (J-sS)" proof -
  have "set_of (K-sS) \<subseteq> set_of (K-s (ds r S))" using assms(2) unfolding diff_def by auto
  moreover have "set_of(K-s (ds r S)) \<subseteq> (dm r J) - (ds r S)" using c unfolding diff_def by auto 
  moreover have "(dm r J) - (ds r S) \<subseteq> dm r (J -s S)" using lemma2_6_1_diff by fast 
  ultimately show ?thesis by auto 
 qed
 show ?thesis using A B C unfolding mul_eq_def by auto
qed

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

(*Lemma 2.6.6*)
lemma lemma2_6_6_a: assumes t: "trans r" and "(M,N) \<in> mul_eq r" shows "(Q + M,Q + N) \<in> 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_of K \<subseteq> dm r J" 
  using assms(2) unfolding union_assoc mul_eq_def by auto
 thus ?thesis using C unfolding mul_eq_def by auto
qed
                
lemma add_left_one: 
 assumes  "\<exists> I J K. {#q#} + N = I + J \<and> {#q#} + M = I + K \<and> (J#\<inter>K={#}) \<and> set_of K \<subseteq> dm r J" 
 shows "\<exists> I2 J K. N = I2 + J \<and> M = I2 + K \<and> set_of K \<subseteq> 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 #\<inter> K = {#})" and D:"set_of K \<subseteq> dm r J" by auto
 have "q\<in>#I" proof (cases "q \<in># I")
  case True thus ?thesis by auto
 next
  case False 
  have "q \<in># J" using False A by (metis count_union multi_member_this neq0_conv plus_nat.add_0)  
  moreover have "q \<in># K" using False B by (metis count_union multi_member_this neq0_conv plus_nat.add_0)
  moreover have "\<not> q \<in># (J #\<inter> K)" using C by auto
  ultimately show ?thesis by auto
 qed
 hence "\<exists> I2. I = {#q#} + I2" by (metis multi_member_split union_commute)
 hence "\<exists> I2. {#q#} + N = ({#q#} + I2) + J \<and> {#q#} + M = ({#q#} + I2) + K" using A B by auto
 thus ?thesis using D by (metis union_assoc diff_union_cancelR union_commute)
qed

lemma lemma2_6_6_b_one : 
assumes "trans r" and "irrefl r" and "({#q#}+M,{#q#}+N) \<in> mul_eq r" shows "(M,N) \<in> 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) \<in> mul_eq r" 
 shows "(M,N) \<in> 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 best
 qed 

lemma lemma2_6_9: assumes t: "trans r" and "(M,N) \<in> mul r" shows "(Q+M,Q+N) \<in> mul r" proof -
 obtain I J K where F1:"N = I + J" and F2:"M = I + K"and F3:"set_of K \<subseteq> dm r J" and F4:"J \<noteq> {#}" 
  using assms unfolding mul_def by auto
 have "Q+N=Q+I+J" and "Q+M=Q+I+K" unfolding F1 F2 union_commute union_lcomm by auto
 thus ?thesis using assms(1) F3 F4 unfolding mul_def by auto
qed
  
(*Lemma 2.6.7*)
lemma lemma2_6_7_a: assumes t: "trans r" and "set_of Q \<subseteq> dm r N - dm r M" and "(M,N) \<in> mul_eq r" 
shows "(Q+M,N) \<in> mul_eq r" proof -
 obtain I J K where A: "N=I+J" and B:"M=I+K" and C:"set_of K \<subseteq> dm r J" using assms unfolding mul_eq_def by auto
 hence "set_of(Q+K) \<subseteq> dm r J" using assms lemma2_6_1_diff unfolding dm_def ds_def by auto
 hence "(I+(Q+K),I+J) \<in> 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 \<subseteq> T" shows "(M -s T,M -s S) \<in> mul_eq r" proof -
 from assms(2) have "(M -s T) \<le> (M -s S)"  
  by (metis Un_absorb2 Un_commute lemmaA_3_10 lemmaA_3_9 mset_le_add_right) 
 thus ?thesis using lemma2_6_2_a[OF t] by auto
qed

(*Def 3.1: lexicographic maximum measure*)
fun lexmax :: "'a rel \<Rightarrow> 'a list \<Rightarrow> 'a multiset" ("(_|_|)") where 
   "r|[]| = {#}"
 | "r|\<alpha>#\<sigma>| =  {#\<alpha>#} + (r|\<sigma>| -s ds r {\<alpha>})" 

lemma lexmax_singleton: "lexmax r [\<alpha>] = {#\<alpha>#}" unfolding lexmax.simps unfolding diff_def by auto

(*Lemma 3.2 *)

(*Lemma 3.2(1)*)
lemma lemma3_2_1: assumes t: "trans r" shows "dm r r|\<sigma>| = dl r \<sigma>" proof (induct \<sigma>)
 case Nil show ?case unfolding dm_def dl_def by auto
 next
 case (Cons \<alpha> \<sigma>)
 have "dm r {#\<alpha>#} \<union> dm r (r|\<sigma>| -s ds r {\<alpha>}) = dm r {#\<alpha>#} \<union> dl r \<sigma>" (is "?L = ?R") proof -
  have "?L \<subseteq> ?R" unfolding Cons[symmetric] diff_def dm_def ds_def by auto
  moreover have "?R \<subseteq> ?L" proof
   fix x assume A: "x \<in> ?R" show "x \<in> ?L" proof (cases "x \<in> dm r {#\<alpha>#}")
    case True thus ?thesis by auto 
   next
    case False 
    hence mem: "x \<in> dm r (lexmax r \<sigma>)" using A Cons by auto 
    have "x \<notin> (ds r (ds r {\<alpha>}))" 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

(* Lemma 3.2(2)*)
lemma lemma3_2_2: "r|\<sigma>@\<tau>| = r|\<sigma>| + (r|\<tau>| -s dl r \<sigma>)" proof(induct \<sigma>)
 case Nil thus ?case unfolding dl_def ds_def lexmax.simps apply auto unfolding diff_empty by auto
 next
 case (Cons \<alpha> \<sigma>)
  have "lexmax r (\<alpha>#\<sigma>@\<tau>) = {#\<alpha>#} + ((lexmax r (\<sigma>@\<tau>)) -s (ds r {\<alpha>}))" by auto
  moreover have "\<dots> = {#\<alpha>#} + ((lexmax r \<sigma> + ((lexmax r \<tau>) -s (dl r \<sigma>))) -s (ds r {\<alpha>}))" 
   using Cons by auto 
  moreover have "\<dots> = {#\<alpha>#} + ((lexmax r \<sigma>) -s (ds r {\<alpha>})) + (((lexmax r \<tau>) -s (dl r \<sigma>)) -s (ds r {\<alpha>}))"
   unfolding lemmaA_3_8 unfolding union_assoc by auto
  moreover have "\<dots> = lexmax r (\<alpha>#\<sigma>) + (((lexmax r \<tau>) -s (dl r \<sigma>)) -s (ds r {\<alpha>}))" by simp
  moreover have "\<dots> = lexmax r (\<alpha>#\<sigma>) + ((lexmax r \<tau>) -s (dl r (\<alpha>#\<sigma>)))" unfolding lemmaA_3_9 dl_def dm_def lemma2_6_1_set[symmetric] by auto
  ultimately show ?case unfolding diff_def by simp
qed

(*Definition 3.3*)

definition D :: "'a rel \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
 "D r \<tau> \<sigma> \<sigma>' \<tau>' = ((r|\<sigma>@\<tau>'|, r|\<tau>| + r|\<sigma>| ) \<in> mul_eq r 
                 \<and> (r|\<tau>@\<sigma>'|, r|\<tau>| + r|\<sigma>| ) \<in> mul_eq r)"

lemma D_eq: assumes "trans r" and "irrefl r" and "D r \<tau> \<sigma> \<sigma>' \<tau>'" 
 shows "(r|\<tau>'| -s dl r \<sigma>,r|\<tau>| ) \<in> mul_eq r" and "(r|\<sigma>'| -s dl r \<tau>,r|\<sigma>| ) \<in> 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|\<tau>'| -s dl r \<sigma>,r|\<tau>| ) \<in> mul_eq r" 
                                                and "(r|\<sigma>'| -s dl r \<tau>,r|\<sigma>| ) \<in> mul_eq r"
 shows "D r \<tau> \<sigma> \<sigma>' \<tau>'" 
 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 \<tau> \<sigma> \<sigma>' \<tau>' = ((r|\<tau>'| -s dl r \<sigma>,r|\<tau>| ) \<in> mul_eq r 
                        \<and> (r|\<sigma>'| -s dl r \<tau>,r|\<sigma>| ) \<in> mul_eq r)"
 using assms D_eq D_inv by auto

lemma mirror_D: assumes "trans r" and "irrefl r" and "D r \<tau> \<sigma> \<sigma>' \<tau>'" shows "D r \<sigma> \<tau> \<tau>' \<sigma>'" 
 using assms D by metis

(*Proposition 3.4*)

definition LD_1' :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
 where "LD_1' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3 = 
 (set \<sigma>1 \<subseteq> ds r {\<beta>} \<and> length \<sigma>2 \<le> 1 \<and> set \<sigma>2 \<subseteq> {\<alpha>} \<and> set \<sigma>3 \<subseteq> ds r {\<alpha>,\<beta>})"

definition LD' :: "'a rel \<Rightarrow> 'a \<Rightarrow> 'a 
  \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" 
 where "LD' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3 \<tau>1 \<tau>2 \<tau>3 = (LD_1' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3 \<and> LD_1' r \<alpha> \<beta> \<tau>1 \<tau>2 \<tau>3)"

(* auxiliary properties on multisets *)

lemma lexmax_le_multiset: assumes t:"trans r" shows "r|\<sigma>| \<le> multiset_of \<sigma>" proof (induct "\<sigma>")
 case Nil thus ?case unfolding lexmax.simps by auto
 next
 case (Cons s \<tau>) hence "lexmax r \<tau> -s ds r {s} \<le> multiset_of \<tau>"
  using lemmaA_3_10 mset_le_add_right order_trans by metis
 thus ?case unfolding multiset_of.simps lexmax.simps using union_commute mset_le_mono_add_left_cancel by metis
qed

lemma split: assumes "LD_1' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3" shows "\<sigma>2 = [] \<or> \<sigma>2 = [\<alpha>]"
 using assms unfolding  LD_1'_def by (cases \<sigma>2) auto

lemma proposition3_4_step: assumes "trans r" and "irrefl r" and "LD_1' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3" 
shows "(r|\<sigma>1@\<sigma>2@\<sigma>3| -s (dm r {#\<beta>#}), r|[\<alpha>]| ) \<in> mul_eq r" proof -
 from assms have "set \<sigma>1 \<subseteq> dm r {#\<beta>#}" unfolding LD'_def LD_1'_def dm_def by auto
 hence "set_of (lexmax r \<sigma>1) \<subseteq> dm r {#\<beta>#}" using submultiset_implies_subset[OF lexmax_le_multiset[OF assms(1)]] by auto
 hence one: "lexmax r \<sigma>1 -s dm r {#\<beta>#} = {#}" using subset_implies_remove_empty by auto
 from assms have "set \<sigma>3 \<subseteq> dl r \<sigma>2 \<union> dl r \<sigma>1 \<union> dm r {#\<beta>#} \<union> dm r {#\<alpha>#}" (is "?l \<subseteq> ?r") unfolding LD'_def LD_1'_def dm_def ds_def by auto
 hence "set_of (lexmax r \<sigma>3) \<subseteq> ?r " using submultiset_implies_subset[OF lexmax_le_multiset[OF assms(1)]] by auto
 hence pre3: "lexmax r \<sigma>3 -s ?r = {#}" using subset_implies_remove_empty by auto
 show ?thesis proof (cases "\<sigma>2 = []")
  case True 
  hence two:"(lexmax r \<sigma>2 -s dl r \<sigma>1) -s dm r {#\<beta>#} = {#}" unfolding diff_def by auto 
  from pre3 have "(((lexmax r \<sigma>3 -s dl r \<sigma>2) -s dl r \<sigma>1) -s dm r {#\<beta>#}) -s dm r {#\<alpha>#} = {#}" unfolding True dl_def lemmaA_3_9 by auto
  hence three:"(((lexmax r \<sigma>3 -s dl r \<sigma>2) -s dl r \<sigma>1) -s dm r {#\<beta>#},{#\<alpha>#}) \<in> 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: "\<sigma>2 = [\<alpha>]" using split[OF assms(3)] by fast
  have two: "((lexmax r \<sigma>2 -s dl r \<sigma>1) -s dm r {#\<beta>#},{#\<alpha>#}) \<in> 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 \<sigma>3 -s ((dl r \<sigma>2 \<union> dm r {#\<alpha>#}) \<union> dl r \<sigma>1 \<union> dm r {#\<beta>#}) = {#}" unfolding eq lemmaA_3_9 using Un_assoc Un_commute by metis
  hence three: "((lexmax r \<sigma>3 -s dl r \<sigma>2) -s dl r \<sigma>1) -s dm r {#\<beta>#} = {#}" 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 \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3 \<tau>1 \<tau>2 \<tau>3"
shows "D r [\<beta>] [\<alpha>] (\<sigma>1@\<sigma>2@\<sigma>3) (\<tau>1@\<tau>2@\<tau>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 "\<alpha> \<in># r|\<sigma>|" shows "\<exists>\<sigma>1 \<sigma>3. (\<sigma>=\<sigma>1@[\<alpha>]@\<sigma>3 \<and> \<alpha> \<notin> dl r \<sigma>1)" 
using assms proof (induct \<sigma>)
 case Nil thus ?case by auto
 next
 case (Cons \<beta> as) thus ?case proof (cases "\<alpha>=\<beta>") 
  case True 
  from this obtain \<sigma>1 \<sigma>3 where dec: "\<beta>#as = \<sigma>1@[\<alpha>]@\<sigma>3" and empty: "\<sigma>1 = []" by auto
  hence "\<alpha> \<notin> dl r \<sigma>1" unfolding dl_def ds_def by auto
  thus ?thesis using dec by auto 
 next
  case False hence "\<alpha> \<in># r|as|-sds r {\<beta>}" using Cons(2) by auto
  hence x: "\<alpha> \<in># r|as| \<and> \<alpha> \<notin> ds r {\<beta>}" unfolding diff_def by (metis count_filter rel_simps(54)) 
  from this obtain \<sigma>1 \<sigma>3 where "as = \<sigma>1 @ [\<alpha>] @ \<sigma>3" and w: "\<alpha> \<notin> dl r \<sigma>1" using Cons(1) by auto
  hence  "\<beta>#as = (\<beta>#\<sigma>1) @ [\<alpha>] @ \<sigma>3" and  "\<alpha> \<notin> dl r (\<beta>#\<sigma>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 \<in> set \<sigma>" and "x \<notin> set_of r|\<sigma>|" 
shows "\<exists>y. (x,y) \<in> r \<and> y \<in> set_of r|\<sigma>|"  using assms(2,3) proof (induct \<sigma>)
 case Nil thus ?case by auto
next
 case (Cons a as) thus ?case proof (cases "x \<notin> set_of r|as|") 
   case True 
   from Cons True obtain y where s: "(x, y) \<in> r \<and> y \<in> set_of r|as|" by auto
   thus ?thesis proof (cases "y \<in> 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_of r|\<sigma>| \<subseteq> ds r S" shows "set \<sigma> \<subseteq> ds r S" proof
 fix x assume A: "x \<in> set \<sigma>" show "x \<in> ds r S" proof (cases "x \<in> set_of r|\<sigma>|")
  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) \<in> r \<and> y \<in> set_of r|\<sigma>|" by auto
  hence "y \<in> 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) \<in> mul_eq r" shows "N = {#}" proof -
 have "(M+N,M+{#}) \<in> mul_eq r" using union_commute assms(3) apply auto using union_commute by metis
 hence k:"(N,{#}) \<in> mul_eq r" using lemma2_6_6_b'[OF assms(1,2)] by fast
 from this obtain I J K where "{#} = I + J \<and> N = I + K \<and> set_of K \<subseteq> dm r J" unfolding mul_eq_def by fast
 thus ?thesis unfolding dm_def ds_def by auto
qed

lemma subset_imp_downset_subset:
assumes "trans r" and "S \<subseteq> ds r T" shows "ds r S \<subseteq> ds r T" proof
 fix x assume A: "x \<in> ds r S" show "x \<in> ds r T" proof -
  from A obtain y where "y \<in> S" and rel1: "(x,y) \<in> r" unfolding ds_def by auto
  hence "y \<in> ds r T" using assms by auto
  from this obtain z where memz: "z \<in> T" and "(y,z) \<in> r" unfolding ds_def by auto
  thus ?thesis using memz transD[OF assms(1) rel1] unfolding ds_def by auto
 qed
qed

lemma proposition3_4_inv_step: 
assumes t: "trans r" and i: "irrefl r" and k:"(r|\<sigma>| -s dl r [\<beta>], {#\<alpha>#}) \<in> mul_eq r" (is "(?M,_) \<in> _")
shows "\<exists> \<sigma>1 \<sigma>2 \<sigma>3. ((\<sigma> = \<sigma>1@\<sigma>2@\<sigma>3) \<and> LD_1' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3)"  proof (cases "\<alpha> \<in># ?M") 
  case True hence "\<alpha> \<in># r|\<sigma>|" unfolding diff_def by (metis count_filter less_not_refl3)
  from this obtain \<sigma>1 \<sigma>3 where sigma: "\<sigma>=\<sigma>1@[\<alpha>]@\<sigma>3" and alpha: "\<alpha> \<notin> dl r \<sigma>1" using lexmax_decompose by metis
  hence dec: "((r|\<sigma>1|-sdl r [\<beta>]) + (r|[\<alpha>]|-s (dl r \<sigma>1 \<union> dl r [\<beta>])) + (r|\<sigma>3| -s (dl r [\<alpha>] \<union> dl r \<sigma>1 \<union> dl r [\<beta>])), {#\<alpha>#}) \<in> mul_eq r" (is "(?M1 + ?M2 + ?M3,_) \<in> _")
   using k unfolding sigma lemma3_2_2 lemmaA_3_8 lemmaA_3_9 LD_1'_def union_assoc by auto

  from True have key: "\<alpha> \<notin> dl r [\<beta>]" unfolding diff_def by (metis (lifting) count_filter less_not_refl)
  hence "?M2 = {#\<alpha>#}" unfolding lexmax_singleton diff_def using alpha by auto
  hence "(?M1+?M3 + {#\<alpha>#},{#\<alpha>#}) \<in> mul_eq r" using dec union_assoc union_commute by metis
  hence w: "?M1+?M3 = {#}" using drop_left_mult_eq assms(1,2) by auto
  from w have "(r|\<sigma>1|-sdl r [\<beta>]) = {#}" by auto
  hence "set_of r|\<sigma>1| \<subseteq> ds r {\<beta>}" using remove_empty_implies_subset unfolding dl_def dm_def by auto
  hence sigma1: "set \<sigma>1 \<subseteq> ds r {\<beta>}" using lexmax_set[OF assms(1)] by auto

  have sigma2: "length [\<alpha>] \<le> 1 \<and> set [\<alpha>] \<subseteq> {\<alpha>}" by auto
 
  have sub:"dl r \<sigma>1 \<subseteq> dl r [\<beta>]" using subset_imp_downset_subset[OF assms(1) sigma1] unfolding dm_def dl_def by auto 
  hence sub2: "dl r \<sigma>1 \<union> dl r [\<beta>] = dl r [\<beta>]" by auto
  from w have  "?M3 = {#}" by auto
  hence "r|\<sigma>3|-s (ds r {\<alpha>} \<union> ds r {\<beta>}) = {#}" unfolding Un_assoc sub2 unfolding dl_def by auto
  hence "r|\<sigma>3|-s (ds r {\<alpha>,\<beta>}) = {#}" unfolding lemma2_6_1_set[symmetric] using insert_is_Un by metis
  hence "set_of r|\<sigma>3| \<subseteq> ds r {\<alpha>,\<beta>}" using remove_empty_implies_subset by auto
  hence sigma3: "set \<sigma>3 \<subseteq> ds r {\<alpha>,\<beta>}" using lexmax_set[OF assms(1)] by auto
  show ?thesis using sigma sigma1 sigma2 sigma3 unfolding LD_1'_def by fast
 next
  case False hence "set_of ?M \<subseteq> dm r {#\<alpha>#}" using mul_eq_singleton[OF k] by auto
  hence "set_of r|\<sigma>| \<subseteq> ds r {\<alpha>,\<beta>}" unfolding diff_def dm_def dl_def ds_def by auto 
  hence "set \<sigma> \<subseteq> ds r {\<alpha>,\<beta>}" using lexmax_set[OF assms(1)] by auto
  thus ?thesis unfolding LD_1'_def by (metis append_Nil bot_least empty_set le0 length_0_conv)
 qed

lemma proposition3_4_inv: 
assumes t: "trans r" and i: "irrefl r" and "D r [\<beta>] [\<alpha>] \<sigma> \<tau>" 
shows "\<exists> \<sigma>1 \<sigma>2 \<sigma>3 \<tau>1 \<tau>2 \<tau>3. (\<sigma> = \<sigma>1@\<sigma>2@\<sigma>3 \<and> \<tau> = \<tau>1@\<tau>2@\<tau>3 \<and> LD' r \<beta> \<alpha> \<sigma>1 \<sigma>2 \<sigma>3 \<tau>1 \<tau>2 \<tau>3)"
using proposition3_4_inv_step[OF assms(1,2)] D_eq[OF assms] unfolding lexmax_singleton LD'_def by metis

(*Lemma 3.5*)
lemma lemma3_5_1: 
assumes t: "trans r" and "irrefl r" and "D r \<tau> \<sigma> \<sigma>' \<tau>'" and "D r \<upsilon> \<sigma>' \<sigma>'' \<upsilon>'" 
shows "(lexmax r (\<tau> @ \<upsilon> @ \<sigma>''), lexmax r (\<tau> @ \<upsilon>) + lexmax r \<sigma>) \<in> mul_eq r" proof -
 have "lexmax r (\<tau> @ \<upsilon> @ \<sigma>'') = (lexmax r (\<tau> @ \<upsilon>) + ((lexmax r \<sigma>'') -s (dl r (\<tau>@\<upsilon>))))" 
  unfolding append_assoc[symmetric] using lemma3_2_2 by fast
 moreover have x:"\<dots> = lexmax r (\<tau>@\<upsilon>) + (((lexmax r \<sigma>'') -s dl r \<upsilon>) -s dl r \<tau>)" 
  unfolding lemma2_6_1_list lemmaA_3_9 Un_commute by auto
 moreover have "(\<dots>,lexmax r (\<tau>@\<upsilon>) + (lexmax r \<sigma>' -s dl r \<tau>)) \<in> mul_eq r" (is "(_,?R) \<in> _")
  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 (\<tau>@\<upsilon>) + lexmax r \<sigma>) \<in> 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 \<tau> \<sigma> \<sigma>' \<tau>'"
shows "(lexmax r (\<sigma>@\<tau>') + (((lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>')) \<inter>s dl r \<tau>)),lexmax r \<sigma> + lexmax r \<tau>) \<in> mul_eq r" (is "(?F+?H,?G) \<in> _")
proof -
 have 1: "(?F,?G) \<in> mul_eq r" using assms(2) unfolding D_def unfolding union_commute by auto
 have 2: "set_of ?H \<subseteq> (dm r ?G) - (dm r ?F)" (is "(?L \<subseteq> _)") proof -
  have "set_of ?H = set_of ((lexmax r \<upsilon>' \<inter>s dl r \<tau>) -s dl r (\<sigma>@\<tau>'))" unfolding lemmaA_3_11 by auto
  moreover have  "\<dots> \<subseteq> (dl r \<tau> - dl r (\<sigma>@\<tau>'))" unfolding diff_def intersect_def by auto 
  moreover have "... \<subseteq> ((dl r \<sigma> \<union> dl r \<tau>) - dl r (\<sigma>@\<tau>'))" 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] unfolding union_commute by auto
qed

lemma step3: assumes t:"trans r" and "D r \<tau> \<sigma> \<sigma>' \<tau>'"
shows "dl r (\<sigma>@\<tau>) \<supseteq> (dm r (lexmax r \<sigma>' + lexmax r \<tau>))" proof -
 have a: "dl r (\<sigma>@\<tau>) = dm r (lexmax r \<tau> + lexmax r \<sigma>)" and b: "dl r (\<tau>@\<sigma>') = dm r (lexmax r \<sigma>' + lexmax r \<tau>)"
   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 \<tau> \<sigma> \<sigma>' \<tau>'"
shows "((lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>')) -s dl r \<tau>, ((lexmax r \<upsilon>' -s dl r \<sigma>') -s dl r \<tau>)) \<in> mul_eq r" (is "(?L,?R) \<in> _")
 proof -
  have "?L = lexmax r \<upsilon>' -s (dl r (\<sigma>@\<tau>'@\<tau>))" unfolding lemmaA_3_9 append_assoc[symmetric] lemma2_6_1_list by auto 
  moreover have "(\<dots>,lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>)) \<in> mul_eq r" (is "(_,?R) \<in> _") using lemma2_6_8[OF t dl_monotone] by auto
  moreover have  "(?R,lexmax r \<upsilon>' -s dm r (lexmax r \<sigma>' + lexmax r \<tau>)) \<in> mul_eq r" (is "(_,?R) \<in> _") using lemma2_6_8[OF t step3[OF assms]] by auto
  moreover have "?R = (lexmax r \<upsilon>' -s dl r \<sigma>') -s dl r \<tau>" 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 \<tau> \<sigma> \<sigma>' \<tau>'" and "D r \<upsilon> \<sigma>' \<sigma>'' \<upsilon>'" 
 shows "(lexmax r (\<sigma> @ \<tau>' @ \<upsilon>'), lexmax r \<sigma> + lexmax r (\<tau>@\<upsilon>)) \<in> mul_eq r" 
proof -
 have 0: "lexmax r (\<sigma>@\<tau>'@\<upsilon>') = lexmax r (\<sigma>@\<tau>') + (lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>'))" (is "?L = _") 
  unfolding append_assoc[symmetric] lemma3_2_2 by auto
 moreover have "\<dots> = lexmax r (\<sigma>@\<tau>') + ((lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>')) \<inter>s dl r \<tau>) + ((lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>')) -s dl r \<tau>)" 
  using lemmaA_3_10 unfolding union_assoc by auto
 moreover have "(\<dots>, lexmax r \<sigma> + lexmax r \<tau> + ((lexmax r \<upsilon>' -s dl r (\<sigma>@\<tau>')) -s dl r \<tau>)) \<in> mul_eq r" (is "(_,?R) \<in> _") 
  using assms claim1 lemma2_6_6_a union_commute by metis
 moreover have "(?R, lexmax r \<sigma> + lexmax r \<tau> + (((lexmax r \<upsilon>' -s dl r \<sigma>') -s dl r \<tau>))) \<in> mul_eq r" (is "(_,?R) \<in> _")
  using lemma2_6_6_a[OF assms(1) claim2[OF assms(1,3)]] by auto
 moreover have "(?R, lexmax r \<sigma> + lexmax r \<tau> + lexmax r \<upsilon> -s dl r \<tau>) \<in> mul_eq r" (is "(_,?R) \<in> _") 
  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 \<sigma> + lexmax r (\<tau>@\<upsilon>)" 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 \<tau> \<sigma> \<sigma>' \<tau>'" and "D r \<upsilon> \<sigma>' \<sigma>'' \<upsilon>'" 
shows "D r (\<tau>@\<upsilon>) \<sigma> \<sigma>'' (\<tau>'@\<upsilon>')" 
 unfolding D_def append_assoc using assms lemma3_5_1 lemma3_5_2 union_commute by metis

lemma step2: assumes "trans r" and "\<tau> \<noteq> []" shows "(M \<inter>s dl r \<tau>,lexmax r \<tau>) \<in> mul r" proof -
 from assms obtain x xs where "\<tau>=x#xs" using list.exhaust by auto
 hence x: "lexmax r \<tau> \<noteq> {#}" by auto
 from assms(2) have y: "set_of (M \<inter>sdl r \<tau>) \<subseteq> dm r (lexmax r \<tau>)" 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



lemma lemma3_6: assumes t: "trans r" and ne: "\<tau> \<noteq> []" and D: "D r \<tau> \<sigma> \<sigma>' \<tau>'" 
shows "(r|\<sigma>'| + r|\<upsilon>|, r|\<sigma>| + r|\<tau>@\<upsilon>| ) \<in> mul r" (is "(?L,?R) \<in> _") proof -
 have "?L = ((lexmax r \<sigma>' + lexmax r \<upsilon>) \<inter>s dl r \<tau>) + ((lexmax r \<sigma>' + lexmax r \<upsilon>) -s dl r \<tau>)" 
  unfolding lemmaA_3_10[symmetric] by auto
 moreover have "(\<dots>,lexmax r \<tau> + ((lexmax r \<sigma>' + lexmax r \<upsilon>) -s dl r \<tau>)) \<in> mul r" (is "(_,?R2) \<in> _") 
  using lemma2_6_9[OF t step2[OF t ne]] union_commute by metis
 moreover have "?R2 = lexmax r \<tau> + (lexmax r \<sigma>' -s dl r \<tau>) + (lexmax r \<upsilon> -s dl r \<tau>)"
  unfolding lemmaA_3_8 union_assoc[symmetric] by auto
 moreover have "\<dots> = lexmax r (\<tau>@\<sigma>') + (lexmax r \<upsilon> -s dl r \<tau>)" unfolding lemma3_2_2 by auto  
 moreover have "(\<dots>,lexmax r \<sigma> + lexmax r \<tau> + (lexmax r \<upsilon> -s dl r \<tau>)) \<in> mul_eq r" (is "(_,?R5) \<in> _") 
  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 "\<sigma> \<noteq> []" and "D r \<tau> \<sigma> \<sigma>' \<tau>'" 
shows "(lexmax r \<tau>' + lexmax r \<upsilon>, lexmax r \<tau> + (lexmax r (\<sigma>@\<upsilon>))) \<in> mul r"
 using assms lemma3_6 mirror_D by fast

(*Theorem 3.7*)
(* labeled rewriting *)
type_synonym ('a,'b) lars = "('a\<times>'b\<times>'a) set"
type_synonym ('a,'b) seq = "('a\<times>('b\<times>'a)list)"

inductive_set seq :: "('a,'b) lars \<Rightarrow> ('a,'b) seq set"
  for ars where "(a,[]) \<in> seq ars" 
            | "(a,\<alpha>,b) \<in> ars \<Longrightarrow> (b,ss) \<in> seq ars \<Longrightarrow> (a,(\<alpha>,b) # ss) \<in> seq ars"

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

(* results on seqs *)
lemma seq_tail1: assumes seq: "(s,x#xs) \<in> seq lars" 
shows "(snd x,xs) \<in> seq lars" and "(s,fst x,snd x) \<in> lars" and "lst (s,x#xs) = lst (snd x,xs)" 
proof -
 show "(snd x,xs)\<in> seq lars" using assms by (cases) auto
next 
 show "(s,fst x,snd x) \<in> 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) \<in> seq ars" shows "(s,ss) \<in> seq ars" "(lst(s,ss),ts) \<in> seq ars" proof -
 show "(s,ss) \<in> 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)) \<in> seq ars" by auto
  from Cons have "(snd x,xs) \<in> 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) \<in> 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) \<in> 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) \<in> seq ars" and "ss2 \<in> seq ars" and "lst (s,ls) = fst ss2"
shows "(s,ls@snd ss2) \<in> seq ars \<and> (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) \<in> seq ars" and mem:"(s,fst x,snd x) \<in> 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 \<in> seq ars" and "ss2 \<in> seq ars" and "lst ss1 = fst ss2"
 shows "(fst ss1,snd ss1@snd ss2) \<in> seq ars" and "(lst (fst ss1,snd ss1@snd ss2) = lst ss2)"
 proof - 
  show "(fst ss1,snd ss1@snd ss2) \<in> 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

(* diagrams *)

definition diagram :: "('a,'b) lars \<Rightarrow> ('a,'b) seq \<times> ('a,'b) seq \<times> ('a,'b) seq \<times> ('a,'b) seq \<Rightarrow> bool"
 where "diagram ars d = (let (\<tau>,\<sigma>,\<sigma>',\<tau>') = d in {\<sigma>,\<tau>,\<sigma>',\<tau>'} \<subseteq> seq ars \<and>
   fst \<sigma> = fst \<tau> \<and> lst \<sigma> = fst \<tau>' \<and> lst \<tau> = fst \<sigma>' \<and> lst \<sigma>' = lst \<tau>')"

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

definition D2 :: "'b rel \<Rightarrow> ('a,'b) seq \<times> ('a,'b) seq \<times> ('a,'b) seq \<times> ('a,'b) seq \<Rightarrow> bool" 
 where "D2 r d = (let (\<tau>,\<sigma>,\<sigma>',\<tau>') = d in D r (labels \<tau>) (labels \<sigma>) (labels \<sigma>') (labels \<tau>'))"

lemma lemma3_5_d: assumes "diagram ars (\<tau>,\<sigma>,\<sigma>',\<tau>')" and "diagram ars (\<upsilon>,\<sigma>',\<sigma>'',\<upsilon>')"
shows "diagram ars ((fst \<tau>,snd \<tau>@snd \<upsilon>),\<sigma>,\<sigma>'',(fst \<tau>'),snd \<tau>'@snd \<upsilon>')" proof -
 from assms have tau: "\<tau> \<in> seq ars" and upsilon: "\<upsilon> \<in> seq ars" and o: "lst \<tau> = fst \<upsilon>" 
            and tau': "\<tau>' \<in> seq ars" and upsilon': "\<upsilon>' \<in> seq ars" and l: "lst \<tau>' = fst \<upsilon>'" 
  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 (\<tau>,\<sigma>,\<sigma>',\<tau>')" and "diagram ars (\<tau>',\<upsilon>,\<upsilon>',\<tau>'')"
shows "diagram ars (\<tau>,(fst \<sigma>,snd \<sigma>@snd \<upsilon>),(fst \<sigma>',snd \<sigma>'@snd \<upsilon>'),\<tau>'')" proof -
 from assms have d1: "diagram ars (\<sigma>,\<tau>,\<tau>',\<sigma>')" and d2: "diagram ars (\<upsilon>,\<tau>',\<tau>'',\<upsilon>')" 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 (\<tau>,\<sigma>,\<sigma>',\<tau>')" and "D2 r (\<upsilon>,\<sigma>',\<sigma>'',\<upsilon>')"
shows "D2 r ((fst \<tau>,snd \<tau>@snd \<upsilon>),\<sigma>,\<sigma>'',(fst \<tau>'),snd \<tau>'@snd \<upsilon>')"
 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 (\<tau>,\<sigma>,\<sigma>',\<tau>')" and "D2 r (\<tau>',\<upsilon>,\<upsilon>',\<tau>'')"
shows "D2 r (\<tau>, (fst \<sigma>,snd \<sigma>@snd \<upsilon>),(fst \<sigma>',snd \<sigma>'@snd \<upsilon>'),\<tau>'')" proof -
 from assms(3,4) have D1:"D2 r (\<sigma>,\<tau>,\<tau>',\<sigma>')" and D2: "D2 r (\<upsilon>,\<tau>',\<tau>'',\<upsilon>')" 
  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 "\<sigma> \<in> seq ars" shows "diagram ars (\<sigma>,(fst \<sigma>,[]),(lst \<sigma>,[]),\<sigma>)"
 using assms seq.intros(1) unfolding diagram_def Let_def lst_def by auto


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

(* lift to combined concept *)
definition DD :: "('a,'b) lars \<Rightarrow> 'b rel \<Rightarrow> ('a,'b) seq \<times> ('a,'b) seq \<times> ('a,'b) seq \<times> ('a,'b) seq \<Rightarrow> bool"
 where "DD ars r d = (diagram ars d \<and> D2 r d)"

lemma lemma3_5_DD: assumes "trans r" and "irrefl r" and "DD ars r (\<tau>,\<sigma>,\<sigma>',\<tau>')" and "DD ars r (\<upsilon>,\<sigma>',\<sigma>'',\<upsilon>')"
shows "DD ars r ((fst \<tau>,snd \<tau>@snd \<upsilon>),\<sigma>,\<sigma>'',(fst \<tau>'),snd \<tau>'@snd \<upsilon>')" 
  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 (\<tau>,\<sigma>,\<sigma>',\<tau>')" and "DD ars r (\<tau>',\<upsilon>,\<upsilon>',\<tau>'')"
shows "DD ars r (\<tau>, (fst \<sigma>,snd \<sigma>@snd \<upsilon>),(fst \<sigma>',snd \<sigma>'@snd \<upsilon>'),\<tau>'')" 
  using assms lemma3_5_d_v lemma3_5'_v unfolding DD_def by fast

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

lemma mirror_DD: assumes "trans r" and "irrefl r" and "DD ars r (\<tau>,\<sigma>,\<sigma>',\<tau>')" shows "DD ars r (\<sigma>,\<tau>,\<tau>',\<sigma>')" 
 using assms mirror_D unfolding DD_def D2_def diagram_def by auto

(* well-foundedness of rel r*)

definition measure :: "'b rel \<Rightarrow> ('a,'b) seq \<times> ('a,'b) seq \<Rightarrow> 'b multiset"
 where "measure r P = lexmax r (labels (fst P)) + lexmax r (labels (snd P))"

definition pex :: "'b rel \<Rightarrow> (('a,'b) seq \<times> ('a,'b) seq) rel"
 where "pex r = {(P1,P2). (measure r P1,measure r P2) \<in> mul r}"

lemma wfi: assumes "relr = pex r" and "\<not> wf (relr)" shows "\<not> wf (mul r)" proof -
 have "\<not> SN ((relr)\<inverse>)" using assms unfolding SN_iff_wf converse_converse by auto 
 from this obtain s where "\<forall>i. (s i, s (Suc i)) \<in> relr\<inverse>" unfolding SN_def SN_on_def by auto
 hence "\<forall>i. (measure r (s i), measure r (s (Suc i))) \<in> (mul r)\<inverse>" unfolding assms(1) pex_def by auto
 hence "\<not> SN ((mul r)\<inverse>)" using chain_imp_not_SN_on unfolding SN_on_def by auto
 thus ?thesis unfolding SN_iff_wf converse_converse .
qed

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

(* main result *)

definition peak :: "('a,'b) lars \<Rightarrow> ('a,'b) seq \<times> ('a,'b) seq \<Rightarrow> bool"
 where "peak ars p = (let (\<tau>,\<sigma>) = p in {\<tau>,\<sigma>} \<subseteq> seq ars \<and> fst \<tau> = fst \<sigma>)"

definition local_peak :: "('a,'b) lars \<Rightarrow> ('a,'b) seq \<times> ('a,'b) seq \<Rightarrow> bool"
 where "local_peak ars p = (let (\<tau>,\<sigma>) = p in peak ars p \<and> length (snd \<tau>) = 1 \<and> length (snd \<sigma>) = 1)"

(*
lemma P_induct: assumes wf: "wf r" and step: "\<And>b.(\<And>a.(a,b) \<in> r \<Longrightarrow> P a) \<Longrightarrow> P b" shows "P b" 
 using wf proof induct case (less a) with step show ?case by fast qed

lemmas P_induct_rule = P_induct[consumes 1, case_names IH, induct pred: peak]
*)

(*proof of Theorem 3.7*)
lemma LD_imp_D: assumes "trans r" and "wf r" and "\<forall>P. (local_peak ars P \<longrightarrow> (\<exists> \<sigma>' \<tau>'. DD ars r (fst P,snd P,\<sigma>',\<tau>')))"
and "peak ars P" shows "(\<exists> \<sigma>' \<tau>'. DD ars r (fst P,snd P,\<sigma>',\<tau>'))" 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 \<tau> \<sigma> where decompose:"P = (\<tau>,\<sigma>)" and tau:"\<tau> \<in> seq ars" and sigma:"\<sigma> \<in> seq ars" 
   and tau_s: "fst \<tau> = s" and sigma_s: "fst \<sigma> = s" using 1 unfolding peak_def apply auto by fast
  show ?case proof (cases "snd \<tau>")
   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 \<beta>_step \<upsilon>_step) 
   hence tau_dec: "\<tau> = (s,[\<beta>_step]@\<upsilon>_step)" apply auto using tau_s surjective_pairing by metis 
   hence tau2:" (s,[\<beta>_step]@\<upsilon>_step) \<in> seq ars" using tau by auto
   show ?thesis proof (cases "snd \<sigma>")
    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 \<alpha>_step \<rho>_step) 
    hence sigma_dec: "\<sigma> = (s,[\<alpha>_step]@\<rho>_step)" apply auto using sigma_s surjective_pairing by metis
    hence sigma2:"(s,[\<alpha>_step]@\<rho>_step) \<in> seq ars" using sigma by auto

    have alpha:"(s,[\<alpha>_step]) \<in> seq ars" (is "?\<alpha> \<in> _") 
     and rho: "(lst (s,[\<alpha>_step]),\<rho>_step) \<in> seq ars" (is "?\<rho> \<in> _") using seq_chop[OF sigma2] by auto
    have beta:"(s,[\<beta>_step]) \<in> seq ars" (is "?\<beta> \<in> _") 
     and upsilon: "(lst (s,[\<beta>_step]),\<upsilon>_step) \<in> seq ars" (is "?\<upsilon> \<in> _") using seq_chop[OF tau2] by auto
    have "local_peak ars (?\<beta>,?\<alpha>)" using alpha beta unfolding local_peak_def peak_def by auto
    from this obtain \<kappa> \<mu> where D:"DD ars r (?\<beta>,?\<alpha>,\<kappa>,\<mu>)" using assms(3) apply auto by metis
    hence kappa: "\<kappa>\<in>seq ars" and mu: "\<mu>\<in>seq ars" unfolding DD_def diagram_def by auto
    have P_IH1: " peak ars (?\<upsilon>,\<kappa>)" using upsilon kappa D unfolding DD_def diagram_def peak_def by auto
    have beta_ne: "labels ?\<beta> \<noteq> []" unfolding labels_def by auto
    have dec: "D r (labels ?\<beta>) (labels ?\<alpha>) (labels \<kappa>) (labels \<mu>)" using D unfolding DD_def D2_def by auto
    have x1:"((?\<upsilon>,\<kappa>), (\<tau>,?\<alpha>)) \<in> pex r" using lemma3_6[OF assms(1) beta_ne dec] 
     unfolding pex_def measure_def decompose labels_def tau_dec apply auto using union_commute by metis
    have "(lexmax r (labels \<tau>) + lexmax r (labels (?\<alpha>)), lexmax r (labels \<tau>) + lexmax r (labels \<sigma>)) \<in> mul_eq r" (is "(?l,?r) \<in> _") 
     unfolding sigma_dec labels_def snd_conv map.simps lexmax.simps diff_from_empty apply auto by (metis lemma2_6_6_a[OF assms(1)] lemma2_6_2_a mset_le_exists_conv assms(1)) 
    hence "((?\<upsilon>,\<kappa>),P) \<in> 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 \<kappa>' \<upsilon>' where IH1: "DD ars r (?\<upsilon>,\<kappa>,\<kappa>',\<upsilon>')" using 1(1)[OF _ P_IH1] unfolding decompose by auto
    hence kappa':"\<kappa>'\<in>seq ars" and upsilon': "\<upsilon>'\<in>seq ars" using D unfolding DD_def diagram_def by auto
    have tau': "(fst \<mu>,snd \<mu>@(snd \<upsilon>')) \<in> seq ars" (is "?\<tau>' \<in> _") using seq_concat(1)[OF mu upsilon'] D IH1 unfolding DD_def diagram_def by auto  
    have DIH1: "DD ars r (\<tau>,?\<alpha>,\<kappa>',?\<tau>')" using lemma3_5_DD[OF assms(1) i D IH1] tau_dec by auto 
    hence dec_dih1: "D r (labels \<tau>) (labels ?\<alpha>) (labels \<kappa>') (labels ?\<tau>')" using DIH1 unfolding DD_def D2_def by simp

    have P_IH2: "peak ars (?\<tau>',?\<rho>)" using tau' rho D unfolding DD_def diagram_def peak_def by auto  
    have alpha_ne: "labels ?\<alpha> \<noteq> []" unfolding labels_def by simp 
    have "((?\<tau>',?\<rho>),P) \<in> 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 \<rho>' \<tau>'' where IH2: "DD ars r (?\<tau>',?\<rho>,\<rho>',\<tau>'')" 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

(*CR with unlabeling*)
definition unlabel :: "('a,'b) lars \<Rightarrow> 'a rel"
 where "unlabel ars = {(a,c). \<exists>b. (a,b,c) \<in> ars}"

lemma step_imp_seq: assumes "(a,b) \<in> (unlabel ars)"  
shows "\<exists>ss \<in> seq ars. fst ss = a \<and> lst ss = b" proof -
 obtain \<alpha> where step:"(a,\<alpha>,b) \<in> ars" using assms unfolding unlabel_def by auto
 hence ss: "(a,[(\<alpha>,b)]) \<in> seq ars" (is "?ss \<in> _") 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) \<in> (unlabel ars)^*"
shows "\<exists>ss \<in> seq ars. fst ss = a \<and> lst ss = b" using assms(1) proof
 fix n assume A: "(a,b) \<in> (unlabel ars)^^n" thus ?thesis proof (induct n arbitrary: a b ars)
 case 0 hence eq: "a = b" by auto
   have "(a,[]) \<in> seq ars" using seq.intros(1) by fast 
  thus ?case using fst_conv lst_def eq by (metis fst_eqD snd_conv) 
 next
 case (Suc m) 
  obtain c where steps: "(a,c) \<in> (unlabel ars)^^m" and step: "(c,b) \<in> (unlabel ars)" using Suc by auto
  obtain ss ts where ss1: "ss \<in> seq ars" and ss2:"fst ss = a"
   and ts1: "ts \<in> 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) \<in> ars" shows "(a,c) \<in> (unlabel ars)" 
 using assms unfolding unlabel_def by auto 

lemma seq_imp_steps:
assumes "ss \<in> seq ars" and "fst ss = a" and "lst ss = b" shows "(a,b) \<in> (unlabel ars)^*" proof -
 from assms surjective_pairing obtain ls where "(a,ls) \<in> 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) \<in> ars" using Cons seq_tail1(2) surjective_pairing by metis
  have "(snd x,b) \<in> (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) \<in> (unlabel ars)^* = (\<exists>ss. fst ss = a \<and> lst ss = b \<and> ss \<in> seq ars)"
 using assms seq_imp_steps steps_imp_seq by metis
 
lemma D_imp_CR: assumes "\<forall>P. (peak ars P \<longrightarrow> (\<exists> \<sigma>' \<tau>'. DD ars r (fst P,snd P,\<sigma>',\<tau>')))" shows "CR (unlabel ars)" proof 
 fix a b c assume A: "(a,b) \<in> (unlabel ars)^*" and B: "(a,c) \<in> (unlabel ars)^*" show "(b,c) \<in> (unlabel ars)\<^sup>\<down>" 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 apply auto by fast
  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 \<in> seq ars" and ss4: "ss4 \<in> 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 \<Rightarrow> 'a rel \<Rightarrow> bool"
 where "LD L ars = (\<exists> (r:: ('b rel)) (lrs::('a,'b) lars). (ars = unlabel lrs) \<and> trans r \<and> wf r \<and> (\<forall>P. (local_peak lrs P \<longrightarrow> (\<exists> \<sigma>' \<tau>'. (DD lrs r (fst P,snd P,\<sigma>',\<tau>'))))))"

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


(*applications*)
lemma measure: 
assumes lab_eq: "lrs = {(a,c,b). c = a \<and> (a,b) \<in> ars}" and "(s,(\<alpha>,t) # ss) \<in> seq lrs"
shows "set (labels (t,ss)) \<subseteq> ds ((ars^+)\<inverse>) {\<alpha>}" using assms(2) proof (induct ss arbitrary: s \<alpha> t )
 case Nil thus ?case unfolding labels_def by auto
next
 case (Cons x xs)
 from this obtain \<beta> u where x:"x = (\<beta>,u)" using surjective_pairing by metis 
 have t: "trans ((ars^+)\<inverse>)" by (metis trans_converse trans_trancl)
 from Cons(1) x have s0: "(s, \<alpha>, t) \<in> lrs" and cs:"(t,(\<beta>,u)#xs) \<in> seq lrs" using Cons.prems seq_tail1(1) snd_conv fst_conv seq_tail1(2) by auto
 have ih: "set (labels (u, xs)) \<subseteq> ds ((ars^+)\<inverse>) {\<beta>}" using Cons(1)[OF cs] by auto
 have key: "{\<beta>} \<subseteq> ds ((ars^+)\<inverse>) {\<alpha>}" using s0 cs seq_tail1(2)[OF cs] unfolding ds_def lab_eq by auto 
 show ?case using ih subset_imp_downset_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 . \<exists> b. (a,b) \<in> ars}" by auto
 from assms obtain lrs where lab_eq: "(lrs  = {(a,c,b). c = a \<and> (a,b) \<in> ars})" by auto 

 have lab: "ars = unlabel lrs" unfolding unlabel_def lab_eq by auto
 have t: "trans ((ars^+)\<inverse>)" using trans_converse trans_trancl by auto
 have w: "wf ((ars^+)\<inverse>)" using assms(2) wf_trancl trancl_converse unfolding SN_iff_wf by metis
 have ps: "\<forall>P. (local_peak lrs P --> (\<exists> \<sigma>' \<tau>'. DD lrs ((ars^+)\<inverse>) (fst P,snd P,\<sigma>',\<tau>')))" proof 
  fix P show "local_peak lrs P --> (\<exists> \<sigma>' \<tau>'. DD lrs ((ars^+)\<inverse>) (fst P,snd P,\<sigma>',\<tau>'))" proof
   assume A: "local_peak lrs P" show "(\<exists> \<sigma>' \<tau>'. DD lrs ((ars^+)\<inverse>) (fst P,snd P,\<sigma>',\<tau>'))" (is "?DD") proof -
    from lab_eq have lab: "ars = unlabel lrs" unfolding unlabel_def by auto
    from A obtain \<tau> \<sigma> where ts: "{\<tau>,\<sigma>} \<subseteq> seq lrs" and l1: "length (snd \<tau>) = 1" and l2: "length (snd \<sigma>) = 1" and P: "P = (\<tau>,\<sigma>)"
     and p: "fst \<tau> = fst \<sigma>" unfolding local_peak_def peak_def by auto

    from l1 obtain \<beta> b where 1: "snd \<tau> = [(\<beta>,b)]" by (metis PairE drop_1_Cons drop_eq_Nil impossible_Cons neq_Nil_conv rel_simps(39))  
    from this obtain a where tau: "\<tau> = (a,[(\<beta>,b)])" by (metis surjective_pairing)
    hence alb: "(a,\<beta>,b) \<in> lrs" using ts by (metis fst_conv insert_subset seq_tail1(2) snd_conv)
    have ab: "(a,b) \<in> ars" and a_eq: "a = \<beta>" using alb unfolding lab_eq by auto

    from l2 obtain \<alpha> c where 2: "snd \<sigma> = [(\<alpha>,c)]" by (metis PairE drop_1_Cons drop_eq_Nil impossible_Cons neq_Nil_conv rel_simps(39))
    hence sigma: "\<sigma> = (a,[(\<alpha>,c)])" using ts by (metis fst_conv p pair_collapse tau)
    hence alc: "(a,\<alpha>,c) \<in> lrs" using ts by (metis fst_conv insert_subset seq_tail1(2) snd_conv)
    hence ac: "(a,c) \<in> ars" and a_eq: "a = \<alpha>" using alb unfolding lab_eq by auto 
    
    from tau sigma have fl: "fst \<tau> = a \<and> fst \<sigma> = a \<and> lst \<tau> = b \<and> lst \<sigma> = c" unfolding lst_def by auto
    from ab ac obtain d where "(b,d) \<in> ars^*" and "(c,d) \<in> ars^*" using assms(1) by auto
    from this obtain \<sigma>' \<tau>' where sigma': "\<sigma>' \<in> seq lrs" and sigma'1: "fst \<sigma>' = b" and "lst \<sigma>' = d"
                           and  tau':"\<tau>' \<in> seq lrs" and "fst \<tau>' = c" and "lst \<tau>' = d" using steps_imp_seq unfolding lab by metis
    hence d:"diagram lrs (fst P, snd P, \<sigma>', \<tau>')" using P A ts fl unfolding local_peak_def peak_def diagram_def by auto

    have s1:"(a,(\<beta>,b)# snd \<sigma>') \<in> seq lrs" using `fst \<sigma>' = b` seq.intros(2)[OF alb] sigma' by auto
    have vv: "set (labels \<sigma>') \<subseteq> ds ((ars^+)\<inverse>) {\<beta>}"  using measure[OF lab_eq s1] by (metis `fst \<sigma>' = b` surjective_pairing)
    have s2:"(a,(\<alpha>,c)# snd \<tau>') \<in> seq lrs" using `fst \<tau>' = c` seq.intros(2)[OF alc] tau' by auto
    hence ww: "set (labels \<tau>') \<subseteq> ds ((ars^+)\<inverse>) {\<alpha>}" using measure[OF lab_eq] s2 by (metis `fst \<tau>' = c` surjective_pairing)
    from w have i: "irrefl ((ars^+)\<inverse>)" by (metis SN_imp_acyclic acyclic_converse acyclic_irrefl assms(2) trancl_converse)
    from vv ww have ld: "LD' ((ars^+)\<inverse>) \<beta> \<alpha> (labels \<sigma>') [] [] (labels \<tau>') [] []" unfolding LD'_def LD_1'_def by auto
    have D: "D ((ars^+)\<inverse>) (labels (fst P)) (labels (snd P)) (labels \<sigma>') (labels \<tau>')" using proposition3_4[OF t i ld] unfolding P sigma tau lst_def labels_def by auto

    from d D have "DD lrs ((ars^+)\<inverse>) (fst P, snd P, \<sigma>', \<tau>')" 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