diff --git a/thys/Knuth_Bendix_Order/Lexicographic_Extension.thy b/thys/Knuth_Bendix_Order/Lexicographic_Extension.thy
--- a/thys/Knuth_Bendix_Order/Lexicographic_Extension.thy
+++ b/thys/Knuth_Bendix_Order/Lexicographic_Extension.thy
@@ -1,995 +1,1019 @@
 section \<open>Lexicographic Extension\<close>
 
 theory Lexicographic_Extension
   imports
     Matrix.Utility
     Order_Pair
 begin
 
 text \<open>
   In this theory we define the lexicographic extension of an order pair, so that it generalizes
   the existing notion @{const lex_prod} which is based on a single order only.
 
   Our main result is that this extension yields again an order pair.
 \<close>
 
 fun lex_two :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel" 
   where
     "lex_two s ns s2 = {((a1, b1), (a2, b2)) . (a1, a2) \<in> s \<or> (a1, a2) \<in> ns \<and> (b1, b2) \<in> s2}"
 
 lemma lex_two:
   assumes compat: "ns O s \<subseteq> s"
     and SN_s: "SN s" 
     and SN_s2: "SN s2"
   shows "SN (lex_two s ns s2)" (is "SN ?r")
 proof
   fix f
   assume "\<forall> i. (f i, f (Suc i)) \<in> ?r"
   then have steps: "\<And> i. (f i, f (Suc i)) \<in> ?r" ..
   let ?a = "\<lambda> i. fst (f i)"
   let ?b = "\<lambda> i. snd (f i)"
   {
     fix i
     from steps[of i]
     have "(?a i, ?a (Suc i)) \<in> s \<or> (?a i, ?a (Suc i)) \<in> ns \<and> (?b i, ?b (Suc i)) \<in> s2"
       by (cases "f i", cases "f (Suc i)", auto)
   }
   note steps = this
   have "\<exists> j. \<forall> i \<ge> j. (?a i, ?a (Suc i)) \<in> ns - s"
     by (rule non_strict_ending[OF _ compat], insert steps SN_s, unfold SN_on_def, auto)
   with steps obtain j where steps: "\<And> i. i \<ge> j \<Longrightarrow> (?b i, ?b (Suc i)) \<in> s2" by auto
   obtain g where g: "g = (\<lambda> i. ?b (j + i))" by auto
   from steps have "\<And> i. (g i, g (Suc i)) \<in> s2" unfolding g by auto
   with SN_s2 show False unfolding SN_defs by auto
 qed
 
 lemma lex_two_compat:
   assumes compat1: "ns1 O s1 \<subseteq> s1"
     and compat1': "s1 O ns1 \<subseteq> s1"
     and trans1: "s1 O s1 \<subseteq> s1"
     and trans1': "ns1 O ns1 \<subseteq> ns1"
     and compat2: "ns2 O s2 \<subseteq> s2"
     and ns: "(ab1, ab2) \<in> lex_two s1 ns1 ns2" 
     and s: "(ab2, ab3) \<in> lex_two s1 ns1 s2"
   shows "(ab1, ab3) \<in> lex_two s1 ns1 s2"
 proof -
   obtain a1 b1 where ab1: "ab1 = (a1, b1)" by force
   obtain a2 b2 where ab2: "ab2 = (a2, b2)" by force
   obtain a3 b3 where ab3: "ab3 = (a3, b3)" by force
   note id = ab1 ab2 ab3
   show ?thesis
   proof (cases "(a1, a2) \<in> s1")
     case s1: True
     show ?thesis 
     proof (cases "(a2, a3) \<in> s1")
       case s2: True
       from trans1 s1 s2 show ?thesis unfolding id by auto
     next
       case False with s have "(a2, a3) \<in> ns1" unfolding id by simp
       from compat1' s1 this show ?thesis unfolding id by auto
     qed
   next
     case False 
     with ns have ns: "(a1, a2) \<in> ns1" "(b1, b2) \<in> ns2" unfolding id by auto
     show ?thesis
     proof (cases "(a2, a3) \<in> s1")
       case s2: True
       from compat1 ns(1) s2 show ?thesis unfolding id by auto
     next
       case False
       with s have nss: "(a2, a3) \<in> ns1" "(b2, b3) \<in> s2" unfolding id by auto
       from trans1' ns(1) nss(1) compat2 ns(2) nss(2)
       show ?thesis unfolding id by auto
     qed
   qed
 qed
 
 lemma lex_two_compat':
   assumes compat1: "ns1 O s1 \<subseteq> s1"
     and compat1': "s1 O ns1 \<subseteq> s1"
     and trans1: "s1 O s1 \<subseteq> s1"
     and trans1': "ns1 O ns1 \<subseteq> ns1"
     and compat2': "s2 O ns2 \<subseteq> s2"
     and s: "(ab1, ab2) \<in> lex_two s1 ns1 s2" 
     and ns: "(ab2, ab3) \<in> lex_two s1 ns1 ns2"
   shows "(ab1, ab3) \<in> lex_two s1 ns1 s2"
 proof -
   obtain a1 b1 where ab1: "ab1 = (a1, b1)" by force
   obtain a2 b2 where ab2: "ab2 = (a2, b2)" by force
   obtain a3 b3 where ab3: "ab3 = (a3, b3)" by force
   note id = ab1 ab2 ab3
   show ?thesis
   proof (cases "(a1, a2) \<in> s1")
     case s1: True
     show ?thesis 
     proof (cases "(a2, a3) \<in> s1")
       case s2: True
       from trans1 s1 s2 show ?thesis unfolding id by auto
     next
       case False with ns have "(a2, a3) \<in> ns1" unfolding id by simp
       from compat1' s1 this show ?thesis unfolding id by auto
     qed
   next
     case False 
     with s have s: "(a1, a2) \<in> ns1" "(b1, b2) \<in> s2" unfolding id by auto
     show ?thesis
     proof (cases "(a2, a3) \<in> s1")
       case s2: True
       from compat1 s(1) s2 show ?thesis unfolding id by auto
     next
       case False
       with ns have nss: "(a2, a3) \<in> ns1" "(b2, b3) \<in> ns2" unfolding id by auto
       from trans1' s(1) nss(1) compat2' s(2) nss(2)
       show ?thesis unfolding id by auto
     qed
   qed
 qed
 
 lemma lex_two_compat2:
   assumes "ns1 O s1 \<subseteq> s1" "s1 O ns1 \<subseteq> s1" "s1 O s1 \<subseteq> s1" "ns1 O ns1 \<subseteq> ns1" "ns2 O s2 \<subseteq> s2"
   shows "lex_two s1 ns1 ns2 O lex_two s1 ns1 s2 \<subseteq> lex_two s1 ns1 s2"
   using lex_two_compat[OF assms] by (intro subsetI, elim relcompE, fast)
 
 lemma lex_two_compat'2:
   assumes "ns1 O s1 \<subseteq> s1" "s1 O ns1 \<subseteq> s1" "s1 O s1 \<subseteq> s1" "ns1 O ns1 \<subseteq> ns1" "s2 O ns2 \<subseteq> s2"
   shows "lex_two s1 ns1 s2 O lex_two s1 ns1 ns2 \<subseteq> lex_two s1 ns1 s2"
   using lex_two_compat'[OF assms] by (intro subsetI, elim relcompE, fast)
 
 lemma lex_two_refl:
   assumes r1: "refl ns1" and r2: "refl ns2"
   shows "refl (lex_two s1 ns1 ns2)"
   using refl_onD[OF r1] and refl_onD[OF r2] by (intro refl_onI) auto
 
 lemma lex_two_order_pair:
   assumes o1: "order_pair s1 ns1" and o2: "order_pair s2 ns2"
   shows "order_pair (lex_two s1 ns1 s2) (lex_two s1 ns1 ns2)"
 proof -
   interpret o1: order_pair s1 ns1 using o1.
   interpret o2: order_pair s2 ns2 using o2.
   note o1.trans_S o1.trans_NS o2.trans_S o2.trans_NS 
     o1.compat_NS_S o2.compat_NS_S o1.compat_S_NS o2.compat_S_NS
   note this [unfolded trans_O_iff]
   note o1.refl_NS o2.refl_NS
   show ?thesis
     by (unfold_locales, intro lex_two_refl, fact+, unfold trans_O_iff)
       (rule lex_two_compat2 lex_two_compat'2;fact)+
 qed
 
 lemma lex_two_SN_order_pair:
   assumes o1: "SN_order_pair s1 ns1" and o2: "SN_order_pair s2 ns2"
   shows "SN_order_pair (lex_two s1 ns1 s2) (lex_two s1 ns1 ns2)"
 proof -
   interpret o1: SN_order_pair s1 ns1 using o1.
   interpret o2: SN_order_pair s2 ns2 using o2.
   note o1.trans_S o1.trans_NS o2.trans_S o2.trans_NS o1.SN o2.SN
     o1.compat_NS_S o2.compat_NS_S o1.compat_S_NS o2.compat_S_NS
   note this [unfolded trans_O_iff]
   interpret order_pair "(lex_two s1 ns1 s2)" "(lex_two s1 ns1 ns2)"
     by(rule lex_two_order_pair, standard)
   show ?thesis by(standard, rule lex_two; fact)
 qed
 
 text \<open>
   In the unbounded lexicographic extension, there is no restriction on the lengths
   of the lists. Therefore it is possible to compare lists of different lengths.
   This usually results a non-terminating relation, e.g., $[1] > [0, 1] > [0, 0, 1] > \ldots$
 \<close>
 
 fun lex_ext_unbounded :: "('a \<Rightarrow> 'a \<Rightarrow> bool \<times> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool \<times> bool"
   where "lex_ext_unbounded f [] [] = (False, True)" |
     "lex_ext_unbounded f (_ # _) [] = (True, True)" |
     "lex_ext_unbounded f [] (_ # _) = (False, False)" |
     "lex_ext_unbounded f (a # as) (b # bs) =
       (let (stri, nstri) = f a b in
       if stri then (True, True)
       else if nstri then lex_ext_unbounded f as bs
       else (False, False))"
 
 lemma lex_ext_unbounded_iff: "(lex_ext_unbounded f xs ys) = (
   ((\<exists> i < length xs. i < length ys \<and> (\<forall> j < i. snd (f (xs ! j) (ys ! j))) \<and> fst (f (xs ! i) (ys !i))) \<or> 
   (\<forall> i < length ys. snd (f (xs ! i) (ys ! i))) \<and> length xs > length ys),
   ((\<exists> i < length xs. i < length ys \<and> (\<forall> j < i. snd (f (xs ! j) (ys ! j))) \<and> fst (f (xs ! i) (ys !i))) \<or> 
   (\<forall> i < length ys. snd (f (xs ! i) (ys ! i))) \<and> length xs \<ge> length ys))
   " (is "?lex xs ys = (?stri xs ys, ?nstri xs ys)")
 proof (induct xs arbitrary: ys)
   case Nil then show ?case by (cases ys, auto)
 next
   case (Cons a as)
   note oCons = this
   from oCons show ?case 
   proof (cases ys, simp)
     case (Cons b bs)
     show ?thesis 
     proof (cases "f a b")
       case (Pair stri nstri)
       show ?thesis
       proof (cases stri)
         case True
         with Pair Cons show ?thesis by auto
       next
         case False        
         show ?thesis 
         proof (cases nstri)
           case False
           with \<open>\<not> stri\<close> Pair Cons show ?thesis by force
         next
           case True
           with False Pair have f: "f a b = (False, True)" by auto
           show ?thesis by (simp add: all_Suc_conv ex_Suc_conv Cons f oCons)
         qed
       qed
     qed
   qed
 qed
 
 declare lex_ext_unbounded.simps[simp del]
 
 text \<open>
   The lexicographic extension of an order pair takes a natural number as maximum bound.
   A decrease with lists of unequal lengths will never be successful if the length of the
   second list exceeds this bound. The bound is essential to preserve strong normalization.
 \<close>
 definition lex_ext :: "('a \<Rightarrow> 'a \<Rightarrow> bool \<times> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool \<times> bool"
   where
     "lex_ext f n ss ts =
       (let lts = length ts in 
       if (length ss = lts \<or> lts \<le> n) then lex_ext_unbounded f ss ts
       else (False, False))"
 
 lemma lex_ext_iff: "(lex_ext f m xs ys) = (
   (length xs = length ys \<or> length ys \<le> m) \<and> ((\<exists> i < length xs. i < length ys \<and> (\<forall> j < i. snd (f (xs ! j) (ys ! j))) \<and> fst (f (xs ! i) (ys !i))) \<or> 
   (\<forall> i < length ys. snd (f (xs ! i) (ys ! i))) \<and> length xs > length ys),
   (length xs = length ys \<or> length ys \<le> m) \<and>
   ((\<exists> i < length xs. i < length ys \<and> (\<forall> j < i. snd (f (xs ! j) (ys ! j))) \<and> fst (f (xs ! i) (ys !i))) \<or> 
   (\<forall> i < length ys. snd (f (xs ! i) (ys ! i))) \<and> length xs \<ge> length ys))
   "
   unfolding lex_ext_def
   by (simp only: lex_ext_unbounded_iff Let_def, auto)
 
 lemma lex_ext_to_lex_ext_unbounded: 
   assumes "length xs \<le> n" and "length ys \<le> n"
   shows "lex_ext f n xs ys = lex_ext_unbounded f xs ys"
   using assms by (simp add: lex_ext_def)
 
 
 lemma lex_ext_stri_imp_nstri: 
   assumes "fst (lex_ext f m xs ys)" 
   shows "snd (lex_ext f m xs ys)"
   using assms by (auto simp: lex_ext_iff)
 
 lemma nstri_lex_ext_map:
   assumes "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> fst (order s t) \<Longrightarrow> fst (order' (f s) (f t))"
     and "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> snd (order s t) \<Longrightarrow> snd (order' (f s) (f t))"
     and "snd (lex_ext order n ss ts)"
   shows "snd (lex_ext order' n (map f ss) (map f ts))"
   using assms unfolding lex_ext_iff by auto
 
 lemma stri_lex_ext_map:
   assumes "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> fst (order s t) \<Longrightarrow> fst (order' (f s) (f t))"
     and "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> snd (order s t) \<Longrightarrow> snd (order' (f s) (f t))"
     and "fst (lex_ext order n ss ts)"
   shows "fst (lex_ext order' n (map f ss) (map f ts))"
   using assms unfolding lex_ext_iff by auto
 
 lemma lex_ext_arg_empty: "snd (lex_ext f n [] xs) \<Longrightarrow> xs = []" 
   unfolding lex_ext_iff by auto
 
 lemma lex_ext_co_compat:
   assumes "\<And> s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> fst (order s t) \<Longrightarrow> snd (order' t s) \<Longrightarrow> False"
     and "\<And> s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> snd (order s t) \<Longrightarrow> fst (order' t s) \<Longrightarrow> False"
     and "\<And> s t. fst (order s t) \<Longrightarrow> snd (order s t)" 
     and "fst (lex_ext order n ss ts)"
     and "snd (lex_ext order' n ts ss)" 
   shows False
 proof -
   let ?ls = "length ss" 
   let ?lt = "length ts"
   define s where "s i = fst (order (ss ! i) (ts ! i))" for i 
   define ns where "ns i = snd (order (ss ! i) (ts ! i))" for i 
   define s' where "s' i = fst (order' (ts ! i) (ss ! i))" for i 
   define ns' where "ns' i = snd (order' (ts ! i) (ss ! i))" for i 
   have co: "i < ?ls \<Longrightarrow> i < ?lt \<Longrightarrow> s i \<Longrightarrow> ns' i \<Longrightarrow> False" for i
     using assms(1) unfolding s_def ns'_def set_conv_nth by auto
   have co': "i < ?ls \<Longrightarrow> i < ?lt \<Longrightarrow> s' i \<Longrightarrow> ns i \<Longrightarrow> False" for i
     using assms(2) unfolding s'_def ns_def set_conv_nth by auto
   from assms(4)[unfolded lex_ext_iff fst_conv, folded s_def ns_def]
   have ch1: "(\<exists> i. i < ?ls \<and> i < ?lt \<and> (\<forall> j<i. ns j) \<and> s i) \<or> (\<forall>i<?lt. ns i) \<and> ?lt < ?ls" (is "?A \<or> ?B") by auto
   from assms(5)[unfolded lex_ext_iff snd_conv, folded s'_def ns'_def]
   have ch2: "(\<exists>i. i < ?ls \<and> i < ?lt \<and> (\<forall>j<i. ns' j) \<and> s' i) \<or> (\<forall>i<?ls. ns' i) \<and> ?ls \<le> ?lt" (is "?A' \<or> ?B'") by auto 
   from ch1 show False
   proof
     assume ?A
     then obtain i where i: "i < ?ls" "i < ?lt" and s: "s i" and ns: "\<And> j. j < i \<Longrightarrow> ns j" by auto
     note s = co[OF i s] 
     have ns: "j < i \<Longrightarrow> s' j \<Longrightarrow> False" for j 
       using i ns[of j] co'[of j] by auto
     from ch2 show False
     proof
       assume ?A'
       then obtain i' where i': "i' < ?ls" "i' < ?lt" and s': "s' i'" and ns': "\<And> j'. j' < i' \<Longrightarrow> ns' j'" by auto
       from s ns'[of i] have "i \<ge> i'" by presburger
       with ns[OF _ s'] have i': "i' = i" by presburger
       from \<open>s i\<close> have "ns i" using assms(3) unfolding s_def ns_def by auto
       from co'[OF i s'[unfolded i'] this] show False .
     next
       assume ?B'
       with i have "ns' i" by auto
       from s[OF this] show False .
     qed
   next
     assume B: ?B
     with ch2 have ?A' by auto
     then obtain i where i: "i < ?ls" "i < ?lt" and s': "s' i" and ns': "\<And> j. j < i \<Longrightarrow> ns' j" by auto
     from co'[OF i s'] B i show False by auto
   qed
 qed
 
 lemma lex_ext_irrefl: assumes "\<And> x. x \<in> set xs \<Longrightarrow> \<not> fst (rel x x)"
   shows "\<not> fst (lex_ext rel n xs xs)" 
 proof 
   assume "fst (lex_ext rel n xs xs)" 
   then obtain i where "i < length xs" and "fst (rel (xs ! i) (xs ! i))" 
     unfolding lex_ext_iff by auto
   with assms[of "xs ! i"] show False by auto
 qed
 
 lemma lex_ext_unbounded_stri_imp_nstri: 
   assumes "fst (lex_ext_unbounded f xs ys)" 
   shows "snd (lex_ext_unbounded f xs ys)"
   using assms by (auto simp: lex_ext_unbounded_iff)
 
 lemma all_nstri_imp_lex_nstri: assumes "\<forall> i < length ys. snd (f (xs ! i) (ys ! i))" and "length xs \<ge> length ys" and "length xs = length ys \<or> length ys \<le> m"
   shows "snd (lex_ext f m xs ys)"
   using assms by (auto simp: lex_ext_iff)
 
 
 lemma lex_ext_cong[fundef_cong]: fixes f g m1 m2 xs1 xs2 ys1 ys2
   assumes "length xs1 = length ys1" and "m1 = m2" and "length xs2 = length ys2" and "\<And> i. \<lbrakk>i < length ys1; i < length ys2\<rbrakk> \<Longrightarrow> f (xs1 ! i) (xs2 ! i) = g (ys1 ! i) (ys2 ! i)" 
   shows "lex_ext f m1 xs1 xs2 = lex_ext g m2 ys1 ys2"
   using assms by (auto simp: lex_ext_iff)
 
 lemma lex_ext_unbounded_cong[fundef_cong]: assumes "as = as'" and "bs = bs'"
   and "\<And> i. i < length as' \<Longrightarrow> i < length bs' \<Longrightarrow> f (as' ! i) (bs' ! i) = g (as' ! i) (bs' ! i)" shows "lex_ext_unbounded f as bs = lex_ext_unbounded g as' bs'"
   unfolding assms lex_ext_unbounded_iff using assms(3) by auto
 
 text \<open>Compatibility is the key property to ensure transitivity of the order.\<close>
 
 text \<open>
   We prove compatibility locally, i.e., it only has to hold for elements
   of the argument lists. Locality is essential for being applicable in recursively
   defined term orders such as KBO.
 \<close>
 lemma lex_ext_compat:
   assumes compat: "\<And> s t u. \<lbrakk>s \<in> set ss; t \<in> set ts; u \<in> set us\<rbrakk> \<Longrightarrow>
     (snd (f s t) \<and> fst (f t u) \<longrightarrow> fst (f s u)) \<and> 
     (fst (f s t) \<and> snd (f t u) \<longrightarrow> fst (f s u)) \<and> 
     (snd (f s t) \<and> snd (f t u) \<longrightarrow> snd (f s u)) \<and>
     (fst (f s t) \<and> fst (f t u) \<longrightarrow> fst (f s u))"
   shows "
     (snd (lex_ext f n ss ts) \<and> fst (lex_ext f n ts us) \<longrightarrow> fst (lex_ext f n ss us)) \<and> 
     (fst (lex_ext f n ss ts) \<and> snd (lex_ext f n ts us) \<longrightarrow> fst (lex_ext f n ss us)) \<and> 
     (snd (lex_ext f n ss ts) \<and> snd (lex_ext f n ts us) \<longrightarrow> snd (lex_ext f n ss us)) \<and>
     (fst (lex_ext f n ss ts) \<and> fst (lex_ext f n ts us) \<longrightarrow> fst (lex_ext f n ss us))
     "
 proof -
   let ?ls = "length ss"
   let ?lt = "length ts"
   let ?lu = "length us"
   let ?st = "lex_ext f n ss ts"
   let ?tu = "lex_ext f n ts us"
   let ?su = "lex_ext f n ss us"
   let ?fst = "\<lambda> ss ts i. fst (f (ss ! i) (ts ! i))"
   let ?snd = "\<lambda> ss ts i. snd (f (ss ! i) (ts ! i))"
   let ?ex = "\<lambda> ss ts. \<exists> i < length ss. i < length ts \<and> (\<forall> j < i. ?snd ss ts j) \<and> ?fst ss ts i"
   let ?all = "\<lambda> ss ts. \<forall> i < length ts. ?snd ss ts i"
   have lengths: "(?ls = ?lt \<or> ?lt \<le> n) \<and> (?lt = ?lu \<or> ?lu \<le> n) \<longrightarrow>
     (?ls = ?lu \<or> ?lu \<le> n)" (is "?lst \<and> ?ltu \<longrightarrow> ?lsu") by arith
   {
     assume st: "snd ?st" and tu: "fst ?tu"
     with lengths have lsu: "?lsu" by (simp add: lex_ext_iff)
     from st have st: "?ex ss ts \<or> ?all ss ts \<and> ?lt \<le> ?ls" by (simp add: lex_ext_iff)
     from tu have tu: "?ex ts us \<or> ?all ts us \<and> ?lu < ?lt" by (simp add: lex_ext_iff)
     from st have "fst ?su"
     proof
       assume st: "?ex ss ts"
       then obtain i1 where i1: "i1 < ?ls \<and> i1 < ?lt" and fst1: "?fst ss ts i1" and snd1: "\<forall> j < i1. ?snd ss ts j" by force
       from tu show ?thesis
       proof
         assume tu: "?ex ts us"
         then obtain i2 where i2: "i2 < ?lt \<and> i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "\<forall> j < i2. ?snd ts us j" by auto
         let ?i = "min i1 i2"
         from i1 i2 have i: "?i < ?ls \<and> ?i < ?lt \<and> ?i < ?lu" by auto
         then have ssi: "ss ! ?i \<in> set ss" and tsi: "ts ! ?i \<in> set ts" and usi: "us ! ?i \<in> set us" by auto
         have snd: "\<forall> j < ?i. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume j: "j < ?i"
           with snd1 snd2 have snd1: "?snd ss ts j" and snd2: "?snd ts us j" by auto
           from j i have ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         have fst: "?fst ss us ?i" 
         proof (cases "i1 < i2")
           case True
           then have "?i = i1" by simp
           with True fst1 snd2 have "?fst ss ts ?i" and "?snd ts us ?i" by auto
           with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
         next
           case False
           show ?thesis 
           proof (cases "i2 < i1")
             case True
             then have "?i = i2" by simp
             with True snd1 fst2 have "?snd ss ts ?i" and "?fst ts us ?i" by auto
             with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
           next
             case False
             with \<open>\<not> i1 < i2\<close> have "i1 = i2" by simp
             with fst1 fst2 have "?fst ss ts ?i" and "?fst ts us ?i" by auto
             with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
           qed
         qed
         show ?thesis by (simp add: lex_ext_iff lsu, rule disjI1, rule exI[of _ ?i], simp add: fst snd i)
       next
         assume tu: "?all ts us \<and> ?lu < ?lt"
         show ?thesis
         proof (cases "i1 < ?lu")
           case True
           then have usi: "us ! i1 \<in> set us" by auto
           from i1 have ssi: "ss ! i1 \<in> set ss" and tsi: "ts ! i1 \<in> set ts" by auto
           from True tu have "?snd ts us i1" by auto
           with fst1 compat[OF ssi tsi usi] have fst: "?fst ss us i1" by auto
           have snd: "\<forall> j < i1. ?snd ss us j"
           proof (intro allI impI)
             fix j
             assume "j < i1"
             with i1 True snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
               ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
             from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
           qed
           with fst lsu True i1 show ?thesis by (auto simp: lex_ext_iff) 
         next
           case False
           with i1 have lus: "?lu < ?ls" by auto
           have snd: "\<forall> j < ?lu. ?snd ss us j"
           proof (intro allI impI)
             fix j
             assume "j < ?lu"
             with False i1 snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
               ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
             from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
           qed
           with lus lsu show ?thesis by (auto simp: lex_ext_iff)
         qed
       qed
     next
       assume st: "?all ss ts \<and> ?lt \<le> ?ls"
       from tu
       show ?thesis
       proof
         assume tu: "?ex ts us"
         with st obtain i2 where i2: "i2 < ?lt \<and> i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "\<forall> j < i2. ?snd ts us j" by auto
         from st i2 have i2: "i2 < ?ls \<and> i2 < ?lt \<and> i2 < ?lu" by auto
         then have ssi: "ss ! i2 \<in> set ss" and tsi: "ts ! i2 \<in> set ts" and usi: "us ! i2 \<in> set us" by auto
         from i2 st have "?snd ss ts i2" by auto
         with fst2 compat[OF ssi tsi usi] have fst: "?fst ss us i2" by auto
         have snd: "\<forall> j < i2. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume "j < i2"
           with i2 snd2 st have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
             ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         with fst lsu i2 show ?thesis by (auto simp: lex_ext_iff)
       next
         assume tu: "?all ts us \<and> ?lu < ?lt"
         with st have lus: "?lu < ?ls" by auto
         have snd: "\<forall> j < ?lu. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume "j < ?lu"
           with st tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
             ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         with lus lsu show ?thesis by (auto simp: lex_ext_iff)
       qed
     qed
   }
   moreover
   {
     assume st: "fst ?st" and tu: "snd ?tu"
     with lengths have lsu: "?lsu" by (simp add: lex_ext_iff)
     from st have st: "?ex ss ts \<or> ?all ss ts \<and> ?lt < ?ls" by (simp add: lex_ext_iff)
     from tu have tu: "?ex ts us \<or> ?all ts us \<and> ?lu \<le> ?lt" by (simp add: lex_ext_iff)
     from st have "fst ?su"
     proof
       assume st: "?ex ss ts"
       then obtain i1 where i1: "i1 < ?ls \<and> i1 < ?lt" and fst1: "?fst ss ts i1" and snd1: "\<forall> j < i1. ?snd ss ts j" by force
       from tu show ?thesis
       proof
         assume tu: "?ex ts us"
         then obtain i2 where i2: "i2 < ?lt \<and> i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "\<forall> j < i2. ?snd ts us j" by auto
         let ?i = "min i1 i2"
         from i1 i2 have i: "?i < ?ls \<and> ?i < ?lt \<and> ?i < ?lu" by auto
         then have ssi: "ss ! ?i \<in> set ss" and tsi: "ts ! ?i \<in> set ts" and usi: "us ! ?i \<in> set us" by auto
         have snd: "\<forall> j < ?i. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume j: "j < ?i"
           with snd1 snd2 have snd1: "?snd ss ts j" and snd2: "?snd ts us j" by auto
           from j i have ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         have fst: "?fst ss us ?i" 
         proof (cases "i1 < i2")
           case True
           then have "?i = i1" by simp
           with True fst1 snd2 have "?fst ss ts ?i" and "?snd ts us ?i" by auto
           with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
         next
           case False
           show ?thesis 
           proof (cases "i2 < i1")
             case True
             then have "?i = i2" by simp
             with True snd1 fst2 have "?snd ss ts ?i" and "?fst ts us ?i" by auto
             with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
           next
             case False
             with \<open>\<not> i1 < i2\<close> have "i1 = i2" by simp
             with fst1 fst2 have "?fst ss ts ?i" and "?fst ts us ?i" by auto
             with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
           qed
         qed
         show ?thesis by (simp add: lex_ext_iff lsu, rule disjI1, rule exI[of _ ?i], simp add: fst snd i)
       next
         assume tu: "?all ts us \<and> ?lu \<le> ?lt"
         show ?thesis
         proof (cases "i1 < ?lu")
           case True
           then have usi: "us ! i1 \<in> set us" by auto
           from i1 have ssi: "ss ! i1 \<in> set ss" and tsi: "ts ! i1 \<in> set ts" by auto
           from True tu have "?snd ts us i1" by auto
           with fst1 compat[OF ssi tsi usi] have fst: "?fst ss us i1" by auto
           have snd: "\<forall> j < i1. ?snd ss us j"
           proof (intro allI impI)
             fix j
             assume "j < i1"
             with i1 True snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
               ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
             from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
           qed
           with fst lsu True i1 show ?thesis by (auto simp: lex_ext_iff) 
         next
           case False
           with i1 have lus: "?lu < ?ls" by auto
           have snd: "\<forall> j < ?lu. ?snd ss us j"
           proof (intro allI impI)
             fix j
             assume "j < ?lu"
             with False i1 snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
               ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
             from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
           qed
           with lus lsu show ?thesis by (auto simp: lex_ext_iff)
         qed
       qed
     next
       assume st: "?all ss ts \<and> ?lt < ?ls"
       from tu
       show ?thesis
       proof
         assume tu: "?ex ts us"
         with st obtain i2 where i2: "i2 < ?lt \<and> i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "\<forall> j < i2. ?snd ts us j" by auto
         from st i2 have i2: "i2 < ?ls \<and> i2 < ?lt \<and> i2 < ?lu" by auto
         then have ssi: "ss ! i2 \<in> set ss" and tsi: "ts ! i2 \<in> set ts" and usi: "us ! i2 \<in> set us" by auto
         from i2 st have "?snd ss ts i2" by auto
         with fst2 compat[OF ssi tsi usi] have fst: "?fst ss us i2" by auto
         have snd: "\<forall> j < i2. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume "j < i2"
           with i2 snd2 st have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
             ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         with fst lsu i2 show ?thesis by (auto simp: lex_ext_iff)
       next
         assume tu: "?all ts us \<and> ?lu \<le> ?lt"
         with st have lus: "?lu < ?ls" by auto
         have snd: "\<forall> j < ?lu. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume "j < ?lu"
           with st tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
             ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         with lus lsu show ?thesis by (auto simp: lex_ext_iff)
       qed
     qed
   }
   moreover
   {
     assume st: "snd ?st" and tu: "snd ?tu"
     with lengths have lsu: "?lsu" by (simp add: lex_ext_iff)
     from st have st: "?ex ss ts \<or> ?all ss ts \<and> ?lt \<le> ?ls" by (simp add: lex_ext_iff)
     from tu have tu: "?ex ts us \<or> ?all ts us \<and> ?lu \<le> ?lt" by (simp add: lex_ext_iff)
     from st have "snd ?su"
     proof
       assume st: "?ex ss ts"
       then obtain i1 where i1: "i1 < ?ls \<and> i1 < ?lt" and fst1: "?fst ss ts i1" and snd1: "\<forall> j < i1. ?snd ss ts j" by force
       from tu show ?thesis
       proof
         assume tu: "?ex ts us"
         then obtain i2 where i2: "i2 < ?lt \<and> i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "\<forall> j < i2. ?snd ts us j" by auto
         let ?i = "min i1 i2"
         from i1 i2 have i: "?i < ?ls \<and> ?i < ?lt \<and> ?i < ?lu" by auto
         then have ssi: "ss ! ?i \<in> set ss" and tsi: "ts ! ?i \<in> set ts" and usi: "us ! ?i \<in> set us" by auto
         have snd: "\<forall> j < ?i. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume j: "j < ?i"
           with snd1 snd2 have snd1: "?snd ss ts j" and snd2: "?snd ts us j" by auto
           from j i have ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         have fst: "?fst ss us ?i" 
         proof (cases "i1 < i2")
           case True
           then have "?i = i1" by simp
           with True fst1 snd2 have "?fst ss ts ?i" and "?snd ts us ?i" by auto
           with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
         next
           case False
           show ?thesis 
           proof (cases "i2 < i1")
             case True
             then have "?i = i2" by simp
             with True snd1 fst2 have "?snd ss ts ?i" and "?fst ts us ?i" by auto
             with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
           next
             case False
             with \<open>\<not> i1 < i2\<close> have "i1 = i2" by simp
             with fst1 fst2 have "?fst ss ts ?i" and "?fst ts us ?i" by auto
             with compat[OF ssi tsi usi] show "?fst ss us ?i" by auto
           qed
         qed
         show ?thesis by (simp add: lex_ext_iff lsu, rule disjI1, rule exI[of _ ?i], simp add: fst snd i)
       next
         assume tu: "?all ts us \<and> ?lu \<le> ?lt"
         show ?thesis
         proof (cases "i1 < ?lu")
           case True
           then have usi: "us ! i1 \<in> set us" by auto
           from i1 have ssi: "ss ! i1 \<in> set ss" and tsi: "ts ! i1 \<in> set ts" by auto
           from True tu have "?snd ts us i1" by auto
           with fst1 compat[OF ssi tsi usi] have fst: "?fst ss us i1" by auto
           have snd: "\<forall> j < i1. ?snd ss us j"
           proof (intro allI impI)
             fix j
             assume "j < i1"
             with i1 True snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
               ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
             from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
           qed
           with fst lsu True i1 show ?thesis by (auto simp: lex_ext_iff) 
         next
           case False
           with i1 have lus: "?lu \<le> ?ls" by auto
           have snd: "\<forall> j < ?lu. ?snd ss us j"
           proof (intro allI impI)
             fix j
             assume "j < ?lu"
             with False i1 snd1 tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
               ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
             from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
           qed
           with lus lsu show ?thesis by (auto simp: lex_ext_iff)
         qed
       qed
     next
       assume st: "?all ss ts \<and> ?lt \<le> ?ls"
       from tu
       show ?thesis
       proof
         assume tu: "?ex ts us"
         with st obtain i2 where i2: "i2 < ?lt \<and> i2 < ?lu" and fst2: "?fst ts us i2" and snd2: "\<forall> j < i2. ?snd ts us j" by auto
         from st i2 have i2: "i2 < ?ls \<and> i2 < ?lt \<and> i2 < ?lu" by auto
         then have ssi: "ss ! i2 \<in> set ss" and tsi: "ts ! i2 \<in> set ts" and usi: "us ! i2 \<in> set us" by auto
         from i2 st have "?snd ss ts i2" by auto
         with fst2 compat[OF ssi tsi usi] have fst: "?fst ss us i2" by auto
         have snd: "\<forall> j < i2. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume "j < i2"
           with i2 snd2 st have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
             ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         with fst lsu i2 show ?thesis by (auto simp: lex_ext_iff)
       next
         assume tu: "?all ts us \<and> ?lu \<le> ?lt"
         with st have lus: "?lu \<le> ?ls" by auto
         have snd: "\<forall> j < ?lu. ?snd ss us j"
         proof (intro allI impI)
           fix j
           assume "j < ?lu"
           with st tu have snd1: "?snd ss ts j" and snd2: "?snd ts us j" and 
             ssj: "ss ! j \<in> set ss" and tsj: "ts ! j \<in> set ts" and usj: "us ! j \<in> set us" by auto
           from compat[OF ssj tsj usj] snd1 snd2 show "?snd ss us j" by auto
         qed
         with lus lsu show ?thesis by (auto simp: lex_ext_iff)
       qed
     qed
   }
   ultimately
   show ?thesis using lex_ext_stri_imp_nstri by blast
 qed
 
 lemma lex_ext_unbounded_map:
   assumes S: "\<And> i. i < length ss \<Longrightarrow> i < length ts \<Longrightarrow> fst (r (ss ! i) (ts ! i)) \<Longrightarrow> fst (r (map f ss ! i) (map f ts ! i))"
     and NS: "\<And> i. i < length ss \<Longrightarrow> i < length ts \<Longrightarrow> snd (r (ss ! i) (ts ! i)) \<Longrightarrow> snd (r (map f ss ! i) (map f ts ! i))"
   shows "(fst (lex_ext_unbounded r ss ts) \<longrightarrow> fst (lex_ext_unbounded r (map f ss) (map f ts))) \<and>
     (snd (lex_ext_unbounded r ss ts) \<longrightarrow> snd (lex_ext_unbounded r (map f ss) (map f ts)))"
   using S NS unfolding lex_ext_unbounded_iff by auto
 
 lemma lex_ext_unbounded_map_S:
   assumes S: "\<And> i. i < length ss \<Longrightarrow> i < length ts \<Longrightarrow> fst (r (ss ! i) (ts ! i)) \<Longrightarrow> fst (r (map f ss ! i) (map f ts ! i))"
     and NS: "\<And> i. i < length ss \<Longrightarrow> i < length ts \<Longrightarrow> snd (r (ss ! i) (ts ! i)) \<Longrightarrow> snd (r (map f ss ! i) (map f ts ! i))"
     and stri: "fst (lex_ext_unbounded r ss ts)"
   shows "fst (lex_ext_unbounded r (map f ss) (map f ts))"
   using lex_ext_unbounded_map[of ss ts r f, OF S NS] stri by blast
 
 lemma lex_ext_unbounded_map_NS:
   assumes S: "\<And> i. i < length ss \<Longrightarrow> i < length ts \<Longrightarrow> fst (r (ss ! i) (ts ! i)) \<Longrightarrow> fst (r (map f ss ! i) (map f ts ! i))"
     and NS: "\<And> i. i < length ss \<Longrightarrow> i < length ts \<Longrightarrow> snd (r (ss ! i) (ts ! i)) \<Longrightarrow> snd (r (map f ss ! i) (map f ts ! i))"
     and nstri: "snd (lex_ext_unbounded r ss ts)"
   shows "snd (lex_ext_unbounded r (map f ss) (map f ts))"
   using lex_ext_unbounded_map[of ss ts r f, OF S NS] nstri by blast
 
 
 
 
 text \<open>Strong normalization with local SN assumption\<close>
 lemma lex_ext_SN:
   assumes compat: "\<And> x y z. \<lbrakk>snd (g x y); fst (g y z)\<rbrakk> \<Longrightarrow> fst (g x z)"
   shows "SN { (ys, xs). (\<forall> y \<in> set ys. SN_on { (s, t). fst (g s t) } {y}) \<and> fst (lex_ext g m ys xs) }" 
     (is "SN { (ys, xs). ?cond ys xs }")
 proof (rule ccontr)
   assume "\<not> ?thesis"
   from this obtain f where f: "\<And> n :: nat. ?cond (f n) (f (Suc n))" unfolding SN_defs by auto
   have m_imp_m: "\<And> n. length (f n) \<le> m \<Longrightarrow> length (f (Suc n)) \<le> m"
   proof -
     fix n
     assume "length (f n) \<le> m"
     then show "length (f (Suc n)) \<le> m"
       using f[of n] by (auto simp: lex_ext_iff)
   qed
   have lm_imp_m_or_eq: "\<And> n. length (f n) > m \<Longrightarrow> length (f (Suc n)) \<le> m \<or> length (f n) = length (f (Suc n))"
   proof -
     fix n
     assume "length (f n) > m"
     then have "\<not> length (f n) \<le> m" by auto
     then show "length (f (Suc n)) \<le> m \<or> length (f n) = length (f (Suc n))"
       using f[of n] by (simp add: lex_ext_iff, blast)
   qed
   let ?l0 = "max (length (f 0)) m"
   have "\<And> n. length (f n) \<le> ?l0"
   proof -
     fix n
     show "length (f n) \<le> ?l0"
     proof (induct n, simp)
       case (Suc n)
       show ?case
       proof (cases "length (f n) \<le> m")
         case True
         with m_imp_m[of n] show ?thesis by auto
       next
         case False
         then have "length (f n) > m" by auto
         with lm_imp_m_or_eq[of n] 
         have "length (f n) = length (f (Suc n)) \<or> length (f (Suc n)) \<le> m" by auto
         with Suc show ?thesis by auto
       qed
     qed
   qed
   from this obtain m' where len: "\<And> n. length (f n) \<le> m'" by auto
   let ?lexgr = "\<lambda> ys xs. fst (lex_ext g m ys xs)"
   let ?lexge = "\<lambda> ys xs. snd (lex_ext g m ys xs)"
   let ?gr = "\<lambda> t s. fst (g t s)"
   let ?ge = "\<lambda> t s. snd (g t s)"
   let ?S = "{ (y, x). fst (g y x) }"
   let ?NS = "{ (y, x). snd (g y x) }"
   let ?baseSN = "\<lambda> ys. \<forall> y \<in> set ys. SN_on ?S {y}"
   let ?con = "\<lambda> ys xs m'. ?baseSN ys \<and> length ys \<le> m' \<and> ?lexgr ys xs"
   let ?confn = "\<lambda> m' f n . ?con (f n) (f (Suc n)) m'"
   from compat have compat2: "?NS O ?S \<subseteq> ?S" by auto
   from f len have  "\<exists> f. \<forall> n. ?confn m' f n" by auto
   then show False
   proof (induct m')
     case 0
     from this obtain f where "?confn 0 f 0" by auto	
     then have "?lexgr [] (f (Suc 0))" by force
     then show False by (simp add: lex_ext_iff)
   next
     case (Suc m')
     from this obtain f where confn: "\<And> n. ?confn (Suc m') f n" by auto
     have ne: "\<And> n. f n \<noteq> []"
     proof -
       fix n
       show "f n \<noteq> []"
       proof (cases "f n")
         case (Cons a b) then show ?thesis by auto
       next
         case Nil
         with confn[of n] show ?thesis by (simp add: lex_ext_iff)
       qed
     qed
     let ?hf = "\<lambda> n. hd (f n)"
     have ge: "\<And> n. ?ge (?hf n) (?hf (Suc n)) \<or> ?gr (?hf n) (?hf (Suc n))"
     proof -
       fix n
       from ne[of n] obtain a as where n: "f n = a # as" by (cases "f n", auto)
       from ne[of "Suc n"] obtain b bs where sn: "f (Suc n) = b # bs" by (cases "f (Suc n)", auto)
       from n sn have "?ge a b \<or> ?gr a b" 
       proof (cases "?gr a b", simp, cases "?ge a b", simp)
         assume "\<not> ?gr a b" and "\<not> ?ge a b" 
         then have g: "g a b = (False, False)" by (cases "g a b", auto)
         from confn[of n] have "fst (lex_ext g m (f n) (f (Suc n)))" (is ?fst) by simp
         have "?fst = False" by (simp add: n sn lex_ext_def g lex_ext_unbounded.simps)
         with \<open>?fst\<close> show "?ge a b \<or> ?gr a b" by simp
       qed
       with n sn show "?ge (?hf n) (?hf (Suc n)) \<or> ?gr (?hf n) (?hf (Suc n))" by simp
     qed
     from ge have GE: "\<forall> n. (?hf n, ?hf (Suc n)) \<in> ?NS \<union> ?S" by auto
     from confn[of 0] ne[of 0] have SN_0: "SN_on ?S {?hf 0}" by (cases "f 0", auto )
     from non_strict_ending[of ?hf, OF GE compat2 SN_0]
     obtain j where j: "\<forall> i \<ge> j. (?hf i, ?hf (Suc i)) \<in> ?NS - ?S" by auto
     let ?h = "\<lambda> n. tl (f (j + n))"
     obtain h where h: "h = ?h"  by auto
     have "\<And> n. ?confn m' h n" 
     proof -
       fix n
       let ?nj = "j + n"
       from spec[OF j, of ?nj]
       have ge_not_gr: "(?hf ?nj, ?hf (Suc ?nj)) \<in> ?NS - ?S" by simp
       from confn[of ?nj] have old: "?confn (Suc m') f ?nj" by simp
       from ne[of ?nj] obtain a as where n: "f ?nj = a # as" by (cases "f ?nj", auto)
       from ne[of "Suc ?nj"] obtain b bs where sn: "f (Suc ?nj) = b # bs" by (cases "f (Suc ?nj)", auto)
       from old have one: "\<forall> y \<in> set (h n). SN_on ?S {y}" 
         by (simp add: h n)
       from old have two: "length (h n) \<le> m'" by (simp add: j n h)
       from ge_not_gr have ge_not_gr2: "g a b = (False, True)"  by (simp add: n sn, cases "g a b", auto)
       from old have "fst (lex_ext g m (f (j+ n)) (f (Suc (j+n))))" (is ?fst) by simp
       then have "length as = length bs \<or> length bs \<le> m" (is ?len)
         by (simp add: lex_ext_def n sn, cases ?len, auto)
       from \<open>?fst\<close>[simplified n sn] have "fst (lex_ext_unbounded g as bs)" (is ?fst)
         by (simp add: lex_ext_def, cases "length as = length bs \<or> Suc (length bs) \<le> m", simp_all add: ge_not_gr2 lex_ext_unbounded.simps)
       then have "fst (lex_ext_unbounded g as bs)" (is ?fst)
         by (simp add: lex_ext_unbounded_iff)
       have three: "?lexgr (h n) (h (Suc n))"
         by (simp add: lex_ext_def h n sn ge_not_gr2 lex_ext_unbounded.simps, simp only: Let_def, simp add: \<open>?len\<close> \<open>?fst\<close>)
       from one two three show "?confn m' h n" by blast
     qed
     with Suc show ?thesis by blast
   qed
 qed
 
 text \<open>Strong normalization with global SN assumption is immediate consequence.\<close>
 lemma lex_ext_SN_2:
   assumes compat: "\<And> x y z. \<lbrakk>snd (g x y); fst (g y z)\<rbrakk> \<Longrightarrow> fst (g x z)"
     and SN:  "SN {(s, t). fst (g s t)}"
   shows "SN { (ys, xs). fst (lex_ext g m ys xs) }" 
 proof -
   from lex_ext_SN[OF compat] 
   have "SN { (ys, xs). (\<forall> y \<in> set ys. SN_on { (s, t). fst (g s t) } {y}) \<and> fst (lex_ext g m ys xs) }" .
   then show ?thesis using SN unfolding SN_on_def by fastforce
 qed
 
 text \<open>The empty list is the least element in the lexicographic extension.\<close>
 lemma lex_ext_least_1: "snd (lex_ext f m xs [])"
   by (simp add: lex_ext_iff)
 
 lemma lex_ext_least_2: "\<not> fst (lex_ext f m [] ys)"
   by (simp add: lex_ext_iff)
 
 text \<open>Preservation of totality on lists of same length.\<close>
 lemma lex_ext_unbounded_total:
   assumes "\<forall>(s, t)\<in>set (zip ss ts). s = t \<or> fst (f s t) \<or> fst (f t s)" 
     and refl: "\<And> t. snd (f t t)" 
     and "length ss = length ts" 
   shows "ss = ts \<or> fst (lex_ext_unbounded f ss ts) \<or> fst (lex_ext_unbounded f ts ss)" 
   using assms(3, 1)
 proof (induct ss ts rule: list_induct2)
   case (Cons s ss t ts)
   from Cons(3) have "s = t \<or> (fst (f s t) \<or> fst (f t s))" by auto
   then show ?case
   proof 
     assume st: "s = t" 
     then show ?thesis using Cons(2-3) refl[of t] by (cases "f t t", auto simp: lex_ext_unbounded.simps)
   qed (auto simp: lex_ext_unbounded.simps split: prod.splits)
 qed simp
 
 lemma lex_ext_total:
   assumes "\<forall>(s, t)\<in>set (zip ss ts). s = t \<or> fst (f s t) \<or> fst (f t s)" 
     and "\<And> t. snd (f t t)" 
     and len: "length ss = length ts" 
   shows "ss = ts \<or> fst (lex_ext f n ss ts) \<or> fst (lex_ext f n ts ss)" 
   using lex_ext_unbounded_total[OF assms] unfolding lex_ext_def Let_def len by auto
 
 text \<open>Monotonicity of the lexicographic extension.\<close>
 lemma lex_ext_unbounded_mono:
   assumes "\<And>i. \<lbrakk>i < length xs; i < length ys; fst (P (xs ! i) (ys ! i))\<rbrakk> \<Longrightarrow> fst (P' (xs ! i) (ys ! i))"
     and   "\<And>i. \<lbrakk>i < length xs; i < length ys; snd (P (xs ! i) (ys ! i))\<rbrakk> \<Longrightarrow> snd (P' (xs ! i) (ys ! i))"
   shows
     "(fst (lex_ext_unbounded P xs ys) \<longrightarrow> fst (lex_ext_unbounded P' xs ys)) \<and>
      (snd (lex_ext_unbounded P xs ys) \<longrightarrow> snd (lex_ext_unbounded P' xs ys))"
     (is "(?l1 xs ys \<longrightarrow> ?r1 xs ys) \<and> (?l2 xs ys \<longrightarrow> ?r2 xs ys)")
   using assms
 proof (induct x\<equiv>P xs ys rule: lex_ext_unbounded.induct)
   note [simp] = lex_ext_unbounded.simps
   case (4 x xs y ys)
   consider (TT) "P x y = (True, True)"
     | (TF) "P x y = (True, False)"
     | (FT) "P x y = (False, True)"
     | (FF) "P x y = (False, False)" by (cases "P x y", auto)
   thus ?case
   proof cases
     case TT
     moreover
     with 4(2) [of 0] and 4(3) [of 0]
     have "P' x y = (True, True)"
       by (auto) (metis (full_types) prod.collapse)
     ultimately
     show ?thesis by simp
   next
     case TF
     show ?thesis
     proof (cases "snd (P' x y)")
       case False
       moreover
       with 4(2) [of 0] and TF
       have "P' x y = (True, False)"
         by (cases "P' x y", auto) 
       ultimately
       show ?thesis by simp
     next
       case True
       with 4(2) [of 0] and TF
       have "P' x y = (True, True)"
         by (auto )(metis (full_types) fst_conv snd_conv surj_pair)
       then show ?thesis by simp
     qed
   next
     case FF then show ?thesis by simp
   next
     case FT
     show ?thesis
     proof (cases "fst (P' x y)")
       case True
       with 4(3) [of 0] and FT
       have *: "P' x y = (True, True)"
         by (auto) (metis (full_types) prod.collapse)
       have "?l1 (x#xs) (y#ys) \<longrightarrow> ?r1 (x#xs) (y#ys)"
         by (simp add: FT *)
       moreover
       have "?l2 (x#xs) (y#ys) \<longrightarrow> ?r2 (x#xs) (y#ys)"
         by (simp add: *)
       ultimately show ?thesis by blast
     next
       case False
       with 4(3) [of 0] and FT
       have *: "P' x y = (False, True)"
         by (cases "P' x y", auto)
       show ?thesis
         using 4(1) [OF refl FT [symmetric]] and 4(2) and 4(3)
         using FT *
         by (auto) (metis Suc_less_eq nth_Cons_Suc)+
     qed
   qed
 qed (simp add: lex_ext_unbounded.simps)+
 
+lemma lex_ext_local_mono [mono]:
+  assumes "\<And>s t. s \<in> set ts \<Longrightarrow> t \<in> set ss \<Longrightarrow> ord s t \<Longrightarrow> ord' s t"
+  shows "fst (lex_ext (\<lambda> x y. (ord x y, (x, y) \<in> ns_rel)) (length ts) ts ss) \<longrightarrow> 
+          fst (lex_ext (\<lambda> x y. (ord' x y, (x, y) \<in> ns_rel)) (length ts) ts ss)"
+proof
+  assume ass: "fst (lex_ext (\<lambda>x y. (ord x y, (x, y) \<in> ns_rel)) (length ts) ts ss)"
+  from assms have mono: "(\<And>i. i < length ts \<Longrightarrow> i < length ss \<Longrightarrow> ord (ts ! i) (ss ! i) \<Longrightarrow> ord' (ts ! i) (ss ! i))"
+    using nth_mem by blast
+  let ?P = "(\<lambda> x y. (ord x y, (x, y) \<in> ns_rel))" 
+  let ?P' = "(\<lambda> x y. (ord' x y, (x, y) \<in> ns_rel))" 
+  from ass have lex: "fst (lex_ext_unbounded ?P ts ss)" unfolding lex_ext_def Let_def if_distrib
+    by (auto split: if_splits)
+  have "fst (lex_ext_unbounded ?P' ts ss)" 
+    by (rule lex_ext_unbounded_mono[THEN conjunct1, rule_format, OF _ _ lex], insert mono, auto)
+  thus "fst (lex_ext (\<lambda>x y. (ord' x y, (x, y) \<in> ns_rel)) (length ts) ts ss)"
+    using ass unfolding lex_ext_def by (auto simp: Let_def)
+qed
+
+lemma lex_ext_mono [mono]:
+  assumes "\<And>s t. ord s t \<longrightarrow> ord' s t"
+  shows "fst (lex_ext (\<lambda> x y. (ord x y, (x, y) \<in> ns)) (length ts) ts ss) \<longrightarrow> 
+          fst (lex_ext (\<lambda> x y. (ord' x y, (x, y) \<in> ns)) (length ts) ts ss)"
+  using assms lex_ext_local_mono[of ts ss ord ord' ns] by blast
+
 end
diff --git a/thys/Weighted_Path_Order/Multiset_Extension2.thy b/thys/Weighted_Path_Order/Multiset_Extension2.thy
--- a/thys/Weighted_Path_Order/Multiset_Extension2.thy
+++ b/thys/Weighted_Path_Order/Multiset_Extension2.thy
@@ -1,1039 +1,1049 @@
 section \<open>Multiset extension of order pairs in the other direction\<close>
 
 text \<open>Many term orders are formulated in the other direction, i.e., they use
   strong normalization of $>$ instead of well-foundedness of $<$. Here, we
   flip the direction of the multiset extension of two orders, connect it to existing interfaces,
   and prove some further properties of the multiset extension.\<close>
 
 theory Multiset_Extension2
   imports
     List_Order
     Multiset_Extension_Pair
 begin
 
 subsection \<open>List based characterization of @{const multpw}\<close>
 
 lemma multpw_listI:
   assumes "length xs = length ys" "X = mset xs" "Y = mset ys"
     "\<forall>i. i < length ys \<longrightarrow> (xs ! i, ys ! i) \<in> ns"
   shows "(X, Y) \<in> multpw ns"
   using assms
 proof (induct xs arbitrary: ys X Y)
   case (Nil ys) then show ?case by (cases ys) (auto intro: multpw.intros)
 next
   case Cons1: (Cons x xs ys' X Y) then show ?case
   proof (cases ys')
     case (Cons y ys)
     then have "\<forall>i. i < length ys \<longrightarrow> (xs ! i, ys ! i) \<in> ns" using Cons1(5) by fastforce
     then show ?thesis using Cons1(2,5) by (auto intro!: multpw.intros simp: Cons(1) Cons1)
   qed auto
 qed
 
 lemma multpw_listE:
   assumes "(X, Y) \<in> multpw ns"
   obtains xs ys where "length xs = length ys" "X = mset xs" "Y = mset ys"
     "\<forall>i. i < length ys \<longrightarrow> (xs ! i, ys ! i) \<in> ns"
   using assms
 proof (induct X Y arbitrary: thesis rule: multpw.induct)
   case (add x y X Y)
   then obtain xs ys where "length xs = length ys" "X = mset xs"
     "Y = mset ys" "(\<forall>i. i < length ys \<longrightarrow> (xs ! i, ys ! i) \<in> ns)" by blast
   then show ?case using add(1) by (intro add(4)[of "x # xs" "y # ys"]) (auto, case_tac i, auto)
 qed auto
 
 subsection\<open>Definition of the multiset extension of $>$-orders\<close>
 
 text\<open>We define here the non-strict extension of the order pair $(\geqslant, >)$ --
   usually written as (ns, s) in the sources --
   by just flipping the directions twice.\<close>
 
 definition ns_mul_ext :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a multiset rel"
   where "ns_mul_ext ns s \<equiv> (mult2_alt_ns (ns\<inverse>) (s\<inverse>))\<inverse>"
 
 lemma ns_mul_extI:
   assumes "A = A1 + A2" and "B = B1 + B2"
     and "(A1, B1) \<in> multpw ns"
     and "\<And>b. b \<in># B2 \<Longrightarrow> \<exists>a. a \<in># A2 \<and> (a, b) \<in> s"
   shows "(A, B) \<in> ns_mul_ext ns s"
   using assms by (auto simp: ns_mul_ext_def multpw_converse intro!: mult2_alt_nsI)
 
 lemma ns_mul_extE:
   assumes "(A, B) \<in> ns_mul_ext ns s"
   obtains A1 A2 B1 B2 where "A = A1 + A2" and "B = B1 + B2"
     and "(A1, B1) \<in> multpw ns"
     and "\<And>b. b \<in># B2 \<Longrightarrow> \<exists>a. a \<in># A2 \<and> (a, b) \<in> s"
   using assms by (auto simp: ns_mul_ext_def multpw_converse elim!: mult2_alt_nsE)
 
 lemmas ns_mul_extI_old = ns_mul_extI[OF _ _ multpw_listI[OF _ refl refl], rule_format]
 
 text\<open>Same for the "greater than" order on multisets.\<close>
 
 definition s_mul_ext :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a multiset rel"
   where "s_mul_ext ns s \<equiv> (mult2_alt_s (ns\<inverse>) (s\<inverse>))\<inverse>"
 
 lemma s_mul_extI:
   assumes "A = A1 + A2" and "B = B1 + B2"
     and "(A1, B1) \<in> multpw ns"
     and "A2 \<noteq> {#}" and "\<And>b. b \<in># B2 \<Longrightarrow> \<exists>a. a \<in># A2 \<and> (a, b) \<in> s"
   shows "(A, B) \<in> s_mul_ext ns s"
   using assms by (auto simp: s_mul_ext_def multpw_converse intro!: mult2_alt_sI)
 
 lemma s_mul_extE:
   assumes "(A, B) \<in> s_mul_ext ns s"
   obtains A1 A2 B1 B2 where "A = A1 + A2" and "B = B1 + B2"
     and "(A1, B1) \<in> multpw ns"
     and "A2 \<noteq> {#}" and "\<And>b. b \<in># B2 \<Longrightarrow> \<exists>a. a \<in># A2 \<and> (a, b) \<in> s"
   using assms by (auto simp: s_mul_ext_def multpw_converse elim!: mult2_alt_sE)
 
 lemmas s_mul_extI_old = s_mul_extI[OF _ _ multpw_listI[OF _ refl refl], rule_format]
 
 
 subsection\<open>Basic properties\<close>
 
 lemma s_mul_ext_mono:
   assumes "ns \<subseteq> ns'" "s \<subseteq> s'" shows "s_mul_ext ns s \<subseteq> s_mul_ext ns' s'"
   unfolding s_mul_ext_def using assms mono_mult2_alt[of "ns\<inverse>" "ns'\<inverse>" "s\<inverse>" "s'\<inverse>"] by simp
 
 lemma ns_mul_ext_mono:
   assumes "ns \<subseteq> ns'" "s \<subseteq> s'" shows "ns_mul_ext ns s \<subseteq> ns_mul_ext ns' s'"
   unfolding ns_mul_ext_def using assms mono_mult2_alt[of "ns\<inverse>" "ns'\<inverse>" "s\<inverse>" "s'\<inverse>"] by simp
 
 lemma s_mul_ext_local_mono:
   assumes sub: "(set_mset xs \<times> set_mset ys) \<inter> ns \<subseteq> ns'" "(set_mset xs \<times> set_mset ys) \<inter> s \<subseteq> s'"
     and rel: "(xs,ys) \<in> s_mul_ext ns s"
   shows "(xs,ys) \<in> s_mul_ext ns' s'"
   using rel s_mul_ext_mono[OF sub] mult2_alt_local[of ys xs False "ns\<inverse>" "s\<inverse>"]
   by (auto simp: s_mul_ext_def converse_Int ac_simps converse_Times)
 
 lemma ns_mul_ext_local_mono:
   assumes sub: "(set_mset xs \<times> set_mset ys) \<inter> ns \<subseteq> ns'" "(set_mset xs \<times> set_mset ys) \<inter> s \<subseteq> s'"
     and rel: "(xs,ys) \<in> ns_mul_ext ns s"
   shows "(xs,ys) \<in> ns_mul_ext ns' s'"
   using rel ns_mul_ext_mono[OF sub] mult2_alt_local[of ys xs True "ns\<inverse>" "s\<inverse>"]
   by (auto simp: ns_mul_ext_def converse_Int ac_simps converse_Times)
 
+lemma s_mul_ext_ord_s [mono]:
+  assumes "\<And>s t. ord s t \<longrightarrow> ord' s t"
+  shows "(s, t) \<in> s_mul_ext ns {(s,t). ord s t} \<longrightarrow> (s, t) \<in> s_mul_ext ns {(s,t). ord' s t}"
+  using assms s_mul_ext_mono by (metis (mono_tags) case_prod_conv mem_Collect_eq old.prod.exhaust subset_eq) 
+
+lemma ns_mul_ext_ord_s [mono]:
+  assumes "\<And>s t. ord s t \<longrightarrow> ord' s t"
+  shows "(s, t) \<in> ns_mul_ext ns {(s,t). ord s t} \<longrightarrow> (s, t) \<in> ns_mul_ext ns {(s,t). ord' s t}"
+  using assms ns_mul_ext_mono by (metis (mono_tags) case_prod_conv mem_Collect_eq old.prod.exhaust subset_eq) 
+
 
 text\<open>The empty multiset is the minimal element for these orders\<close>
 
 lemma ns_mul_ext_bottom: "(A,{#}) \<in> ns_mul_ext ns s"
   by (auto intro!: ns_mul_extI)
 
 lemma ns_mul_ext_bottom_uniqueness:
   assumes "({#},A) \<in> ns_mul_ext ns s"
   shows "A = {#}"
   using assms by (auto simp: ns_mul_ext_def mult2_alt_ns_def)
 
 lemma ns_mul_ext_bottom2:
   assumes "(A,B) \<in> ns_mul_ext ns s"
     and "B \<noteq> {#}"
   shows "A \<noteq> {#}"
   using assms by (auto simp: ns_mul_ext_def mult2_alt_ns_def)
 
 lemma s_mul_ext_bottom:
   assumes "A \<noteq> {#}"
   shows "(A,{#}) \<in> s_mul_ext ns s"
   using assms by (auto simp: s_mul_ext_def mult2_alt_s_def)
 
 lemma s_mul_ext_bottom_strict:
   "({#},A) \<notin> s_mul_ext ns s"
   by (auto simp: s_mul_ext_def mult2_alt_s_def)
 
 text\<open>Obvious introduction rules.\<close>
 
 lemma all_ns_ns_mul_ext:
   assumes "length as = length bs"
     and "\<forall>i. i < length bs \<longrightarrow> (as ! i, bs ! i) \<in> ns"
   shows "(mset as, mset bs) \<in> ns_mul_ext ns s"
   using assms by (auto intro!: ns_mul_extI[of _ _ "{#}" _ _ "{#}"] multpw_listI)
 
 lemma all_s_s_mul_ext:
   assumes "A \<noteq> {#}"
     and "\<forall>b. b \<in># B \<longrightarrow> (\<exists>a. a \<in># A \<and> (a,b) \<in> s)"
   shows "(A, B) \<in> s_mul_ext ns s"
   using assms by (auto intro!: s_mul_extI[of _ "{#}" _ _ "{#}"] multpw_listI)
 
 text\<open>Being stricly lesser than implies being lesser than\<close>
 
 lemma s_ns_mul_ext:
   assumes "(A, B) \<in> s_mul_ext ns s"
   shows "(A, B) \<in> ns_mul_ext ns s"
   using assms by (simp add: s_mul_ext_def ns_mul_ext_def mult2_alt_s_implies_mult2_alt_ns)
 
 text\<open>The non-strict order is reflexive.\<close>
 
 lemma multpw_refl':
   assumes "locally_refl ns A"
   shows "(A, A) \<in> multpw ns"
 proof -
   have "Restr Id (set_mset A) \<subseteq> ns" using assms by (auto simp: locally_refl_def)
   from refl_multpw[of Id] multpw_local[of A A Id] mono_multpw[OF this]
   show ?thesis by (auto simp: refl_on_def)
 qed
 
 lemma ns_mul_ext_refl_local:
   assumes "locally_refl ns A"
   shows "(A, A) \<in> ns_mul_ext ns s"
   using assms by (auto intro!:  ns_mul_extI[of A A "{#}" A A "{#}" ns s] multpw_refl')
 
 lemma ns_mul_ext_refl:
   assumes "refl ns"
   shows "(A, A) \<in> ns_mul_ext ns s"
   using assms ns_mul_ext_refl_local[of ns A s] unfolding refl_on_def locally_refl_def by auto
 
 text\<open>The orders are union-compatible\<close>
 
 lemma ns_s_mul_ext_union_multiset_l:
   assumes "(A, B) \<in> ns_mul_ext ns s"
     and "C \<noteq> {#}"
     and "\<forall>d. d \<in># D \<longrightarrow> (\<exists>c. c \<in># C \<and> (c,d) \<in> s)"
   shows "(A + C, B + D) \<in> s_mul_ext ns s"
   using assms unfolding ns_mul_ext_def s_mul_ext_def
   by (auto intro!: converseI mult2_alt_ns_s_add mult2_alt_sI[of _ "{#}" _ _ "{#}"])
 
 lemma s_mul_ext_union_compat:
   assumes "(A, B) \<in> s_mul_ext ns s"
     and "locally_refl ns C"
   shows "(A + C, B + C) \<in> s_mul_ext ns s"
   using assms ns_mul_ext_refl_local[OF assms(2)] unfolding ns_mul_ext_def s_mul_ext_def
   by (auto intro!: converseI mult2_alt_s_ns_add)
 
 lemma ns_mul_ext_union_compat:
   assumes "(A, B) \<in> ns_mul_ext ns s"
     and "locally_refl ns C"
   shows "(A + C, B + C) \<in> ns_mul_ext ns s"
   using assms ns_mul_ext_refl_local[OF assms(2)] unfolding ns_mul_ext_def s_mul_ext_def
   by (auto intro!: converseI mult2_alt_ns_ns_add)
 
 context
   fixes NS :: "'a rel"
   assumes NS: "refl NS"
 begin
 
 lemma refl_imp_locally_refl: "locally_refl NS A" using NS unfolding refl_on_def locally_refl_def by auto
 
 lemma supseteq_imp_ns_mul_ext:
   assumes "A \<supseteq># B"
   shows "(A, B) \<in> ns_mul_ext NS S"
   using assms
   by (auto intro!: ns_mul_extI[of A B "A - B" B B "{#}"] multpw_refl' refl_imp_locally_refl
       simp: subset_mset.add_diff_inverse)
 
 lemma supset_imp_s_mul_ext:
   assumes "A \<supset># B"
   shows "(A, B) \<in> s_mul_ext NS S"
   using assms subset_mset.add_diff_inverse[of B A]
   by (auto intro!: s_mul_extI[of A B "A - B" B B "{#}"] multpw_refl' refl_imp_locally_refl
       simp: Diff_eq_empty_iff_mset)
 
 end
 
 definition mul_ext :: "('a \<Rightarrow> 'a \<Rightarrow> bool \<times> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool \<times> bool"
   where "mul_ext f xs ys \<equiv> let s = {(x,y). fst (f x y)}; ns = {(x,y). snd (f x y)}
     in ((mset xs,mset ys) \<in> s_mul_ext ns s, (mset xs, mset ys) \<in> ns_mul_ext ns s)"
 
 definition "smulextp f m n \<longleftrightarrow> (m, n) \<in> s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
 definition "nsmulextp f m n \<longleftrightarrow> (m, n) \<in> ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
 
 lemma smulextp_cong[fundef_cong]:
   assumes "xs1 = ys1"
     and "xs2 = ys2"
     and "\<And> x x'. x \<in># ys1 \<Longrightarrow> x' \<in># ys2 \<Longrightarrow> f x x' = g x x'"
   shows "smulextp f xs1 xs2 = smulextp g ys1 ys2"
   unfolding smulextp_def
 proof
   assume "(xs1, xs2) \<in> s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
   from s_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (g x y)}" "{(x, y). fst (g x y)}"]
   show "(ys1, ys2) \<in> s_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
     using assms by force
 next
   assume "(ys1, ys2) \<in> s_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
   from s_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (f x y)}" "{(x, y). fst (f x y)}"]
   show "(xs1, xs2) \<in> s_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
     using assms by force
 qed
 
 lemma nsmulextp_cong[fundef_cong]:
   assumes "xs1 = ys1"
     and "xs2 = ys2"
     and "\<And> x x'. x \<in># ys1 \<Longrightarrow> x' \<in># ys2 \<Longrightarrow> f x x' = g x x'"
   shows "nsmulextp f xs1 xs2 = nsmulextp g ys1 ys2"
   unfolding nsmulextp_def
 proof
   assume "(xs1, xs2) \<in> ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
   from ns_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (g x y)}" "{(x, y). fst (g x y)}"]
   show "(ys1, ys2) \<in> ns_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
     using assms by force
 next
   assume "(ys1, ys2) \<in> ns_mul_ext {(x, y). snd (g x y)} {(x, y). fst (g x y)}"
   from ns_mul_ext_local_mono[OF _ _ this, of "{(x, y). snd (f x y)}" "{(x, y). fst (f x y)}"]
   show "(xs1, xs2) \<in> ns_mul_ext {(x, y). snd (f x y)} {(x, y). fst (f x y)}"
     using assms by force
 qed
 
 
 definition "mulextp f m n = (smulextp f m n, nsmulextp f m n)"
 
 lemma mulextp_cong[fundef_cong]:
   assumes "xs1 = ys1"
     and "xs2 = ys2"
     and "\<And> x x'. x \<in># ys1 \<Longrightarrow> x' \<in># ys2 \<Longrightarrow> f x x' = g x x'"
   shows "mulextp f xs1 xs2 = mulextp g ys1 ys2"
   unfolding mulextp_def using assms by (auto cong: nsmulextp_cong smulextp_cong)
 
 lemma mset_s_mul_ext:
   "(mset xs, mset ys) \<in> s_mul_ext {(x, y). snd (f x y)} {(x, y).fst (f x y)} \<longleftrightarrow>
     fst (mul_ext f xs ys)"
   by (auto simp: mul_ext_def Let_def)
 
 lemma mset_ns_mul_ext:
   "(mset xs, mset ys) \<in> ns_mul_ext {(x, y). snd (f x y)} {(x, y).fst (f x y)} \<longleftrightarrow>
     snd (mul_ext f xs ys)"
   by (auto simp: mul_ext_def Let_def)
 
 lemma smulextp_mset_code:
   "smulextp f (mset xs) (mset ys) \<longleftrightarrow> fst (mul_ext f xs ys)"
   unfolding smulextp_def mset_s_mul_ext ..
 
 lemma nsmulextp_mset_code:
   "nsmulextp f (mset xs) (mset ys) \<longleftrightarrow> snd (mul_ext f xs ys)"
   unfolding nsmulextp_def mset_ns_mul_ext ..
 
 lemma nstri_mul_ext_map:
   assumes "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> fst (order s t) \<Longrightarrow> fst (order' (f s) (f t))"
     and "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> snd (order s t) \<Longrightarrow> snd (order' (f s) (f t))"
     and "snd (mul_ext order ss ts)"
   shows "snd (mul_ext order' (map f ss) (map f ts))"
   using assms mult2_alt_map[of "mset ts" "mset ss" "{(t, s). snd (order s t)}" f f
       "{(t, s). snd (order' s t)}" "{(t, s). fst (order s t)}" "{(t, s). fst (order' s t)}" True]
   by (auto simp: mul_ext_def ns_mul_ext_def converse_unfold)
 
 lemma stri_mul_ext_map:
   assumes "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> fst (order s t) \<Longrightarrow> fst (order' (f s) (f t))"
     and "\<And>s t. s \<in> set ss \<Longrightarrow> t \<in> set ts \<Longrightarrow> snd (order s t) \<Longrightarrow> snd (order' (f s) (f t))"
     and "fst (mul_ext order ss ts)"
   shows "fst (mul_ext order' (map f ss) (map f ts))"
   using assms mult2_alt_map[of "mset ts" "mset ss" "{(t,s). snd (order s t)}" f f
       "{(t, s). snd (order' s t)}" "{(t, s). fst (order s t)}" "{(t, s). fst (order' s t)}" False]
   by (auto simp: mul_ext_def s_mul_ext_def converse_unfold)
 
 
 lemma mul_ext_arg_empty: "snd (mul_ext f [] xs) \<Longrightarrow> xs = []" 
   unfolding mul_ext_def Let_def by (auto simp: ns_mul_ext_def mult2_alt_def)
 
 
 text \<open>The non-strict order is irreflexive\<close>
 lemma s_mul_ext_irrefl: assumes irr: "irrefl_on (set_mset A) S" 
   and S_NS: "S \<subseteq> NS" 
   and compat: "S O NS \<subseteq> S" 
 shows "(A,A) \<notin> s_mul_ext NS S" using irr
 proof (induct A rule: wf_induct[OF wf_measure[of size]])
   case (1 A)
   show ?case
   proof
     assume "(A,A) \<in> s_mul_ext NS S" 
     from s_mul_extE[OF this]
     obtain A1 A2 B1 B2 where
       A: "A = A1 + A2" 
       and B: "A = B1 + B2"
       and AB1: "(A1, B1) \<in> multpw NS"
       and ne: "A2 \<noteq> {#}" 
       and S: "\<And>b. b \<in># B2 \<Longrightarrow> \<exists>a. a \<in># A2 \<and> (a, b) \<in> S" 
       by blast
     from multpw_listE[OF AB1] obtain as1 bs1 where
       l1: "length as1 = length bs1" 
       and A1: "A1 = mset as1" 
       and B1: "B1 = mset bs1" 
       and NS: "\<And> i. i<length bs1 \<Longrightarrow> (as1 ! i, bs1 ! i) \<in> NS" by blast
     (* store for later usage *)
     note NSS = NS
     note SS = S
    
     obtain as2 where A2: "A2 = mset as2" by (metis ex_mset)
     obtain bs2 where B2: "B2 = mset bs2" by (metis ex_mset)
     define as where "as = as1 @ as2" 
     define bs where "bs = bs1 @ bs2" 
     have as: "A = mset as" unfolding A A1 A2 as_def by simp
     have bs: "A = mset bs" unfolding B B1 B2 bs_def by simp
     from as bs have abs: "mset as = mset bs" by simp
     hence set_ab: "set as = set bs" by (rule mset_eq_setD)
     let ?n = "length bs" 
     have las: "length as = ?n" 
       using mset_eq_length abs by fastforce
     let ?m = "length bs1" 
     define decr where "decr j i \<equiv> 
        (as ! j, bs ! i) \<in> NS \<and> (i < ?m \<longrightarrow> j = i) \<and> (?m \<le> i \<longrightarrow> ?m \<le> j \<and> (as ! j, bs ! i) \<in> S)" for i j
     define step where "step i j k = 
        (i < ?n \<and> j < ?n \<and> k < ?n \<and> bs ! k = as ! j \<and> decr j i)" 
       for i j k
     {
       fix i
       assume i: "i < ?n" 
       let ?b = "bs ! i" 
       have "\<exists> j. j < ?n \<and> decr j i" 
       proof (cases "i < ?m")
         case False
         with i have "?b \<in> set bs2" unfolding bs_def 
           by (auto simp: nth_append)
         hence "?b \<in># B2" unfolding B2 by auto
         from S[OF this, unfolded A2] obtain a where a: "a \<in> set as2" and S: "(a, ?b) \<in> S" 
           by auto
         from a obtain k where a: "a = as2 ! k" and k: "k < length as2" unfolding set_conv_nth by auto
         have "a = as ! (?m + k)" unfolding a as_def l1[symmetric] by simp
         from S[unfolded this] S_NS False k
         show ?thesis unfolding decr_def
           by (intro exI[of _ "?m + k"], auto simp: las[symmetric] l1[symmetric] as_def)
       next
         case True
         from NS[OF this] i True show ?thesis unfolding decr_def
           by (auto simp: as_def bs_def l1 nth_append)
       qed (insert i NS)
       from this[unfolded set_conv_nth] las
       obtain j where j: "j < ?n" and decr: "decr j i" by auto
       let ?a = "as ! j" 
       from j las have "?a \<in> set as" by auto
       from this[unfolded set_ab, unfolded set_conv_nth] obtain k where
         k: "k < ?n" and id: "?a = bs ! k" by auto
       have "\<exists> j k. step i j k" 
         using j k decr id i unfolding step_def by metis
     }
     hence "\<forall> i. \<exists> j k. i < ?n \<longrightarrow> step i j k" by blast
     from choice[OF this] obtain J' where "\<forall> i. \<exists> k. i < ?n \<longrightarrow> step i (J' i) k" by blast
     from choice[OF this] obtain K' where 
       step: "\<And> i. i < ?n \<Longrightarrow> step i (J' i) (K' i)" by blast
     define I where "I i = (K'^^i) 0" for i 
     define J where "J i = J' (I i)" for i
     define K where "K i = K' (I i)" for i
     from ne have "A \<noteq> {#}" unfolding A by auto
     hence "set as \<noteq> {}" unfolding as by auto
     hence "length as \<noteq> 0" by simp
     hence n0: "0 < ?n" using las by auto
     {
       fix n
       have "step (I n) (J n) (K n)" 
       proof (induct n)
         case 0
         from step[OF n0] show ?case unfolding I_def J_def K_def by auto
       next
         case (Suc n)
         from Suc have "K n < ?n" unfolding step_def by auto
         from step[OF this] show ?case unfolding J_def K_def I_def by auto
       qed
     }
     note step = this
     have "I n \<in> {..<?n}" for n using step[of n] unfolding step_def by auto 
     hence "I ` UNIV \<subseteq> {..<?n}" by auto
     from finite_subset[OF this] have "finite (I ` UNIV)" by simp
     from pigeonhole_infinite[OF _ this] obtain m where 
       "infinite {i. I i = I m}" by auto
     hence "\<exists> m'. m' > m \<and> I m' = I m"
       by (simp add: infinite_nat_iff_unbounded)
     then obtain m' where *: "m < m'" "I m' = I m" by auto
     let ?P = "\<lambda> n. \<exists> m. n \<noteq> 0 \<and> I (n + m) = I m" 
     define n where "n = (LEAST n. ?P n)" 
     have "\<exists> n. ?P n" 
       by (rule exI[of _ "m' - m"], rule exI[of _ m], insert *, auto)
     from LeastI_ex[of ?P, OF this, folded n_def]
     obtain m where n: "n \<noteq> 0" and Im: "I (n + m) = I m" by auto
     let ?M = "{m..<m+n}" 
     {
       fix i j
       assume *: "m \<le> i" "i < j" "j < n + m" 
       define k where "k = j - i" 
       have k0: "k \<noteq> 0" and j: "j = k + i" and kn: "k < n" using * unfolding k_def by auto
       from not_less_Least[of _ ?P, folded n_def, OF kn] k0
       have "I i \<noteq> I j" unfolding j by metis
     } 
     hence inj: "inj_on I ?M" unfolding inj_on_def
       by (metis add.commute atLeastLessThan_iff linorder_neqE_nat)
     define b where "b i = bs ! I i" for i
     have bnm: "b (n + m) = b m" unfolding b_def Im ..
     {
       fix i
       from step[of i, unfolded step_def]
       have id: "bs ! K i = as ! J i" and decr: "decr (J i) (I i)" by auto
       from id decr[unfolded decr_def] have "(bs ! K i, bs ! I i) \<in> NS" by auto
       also have "K i = I (Suc i)" unfolding I_def K_def by auto
       finally have "(b (Suc i), b i) \<in> NS" unfolding b_def by auto
     } note NS = this
     {
       fix i j :: nat
       assume "i \<le> j" 
       then obtain k where j: "j = i + k" by (rule less_eqE)
       have "(b j, b i) \<in> NS^*" unfolding j
       proof (induct k)
         case (Suc k)
         thus ?case using NS[of "i + k"] by auto
       qed auto
     } note NSstar = this
     {
       assume "\<exists> i \<in> ?M. I i \<ge> ?m" 
       then obtain k where k: "k \<in> ?M" and I: "I k \<ge> ?m" by auto
       from step[of k, unfolded step_def]
       have id: "bs ! K k = as ! J k" and decr: "decr (J k) (I k)" by auto
       from id decr[unfolded decr_def] I have "(bs ! K k, bs ! I k) \<in> S" by auto
       also have "K k = I (Suc k)" unfolding I_def K_def by auto
       finally have S: "(b (Suc k), b k) \<in> S" unfolding b_def by auto
       from k have "m \<le> k" by auto
       from NSstar[OF this] have NS1: "(b k, b m) \<in> NS^*" .
       from k have "Suc k \<le> n + m" by auto
       from NSstar[OF this, unfolded bnm] have NS2: "(b m, b (Suc k)) \<in> NS^*" .
       from NS1 NS2 have "(b k, b (Suc k)) \<in> NS^*" by simp
       with S have "(b (Suc k), b (Suc k)) \<in> S O NS^*" by auto
       also have "\<dots> \<subseteq> S" using compat
         by (metis compat_tr_compat converse_inward(1) converse_mono converse_relcomp)
       finally have contradiction: "b (Suc k) \<notin> set_mset A" using 1 unfolding irrefl_on_def by auto
       have "b (Suc k) \<in> set bs" unfolding b_def using step[of "Suc k"] unfolding step_def
         by auto
       also have "set bs = set_mset A" unfolding bs by auto
       finally have False using contradiction by auto
     }
     hence only_NS: "i \<in> ?M \<Longrightarrow> I i < ?m" for i by force
     {
       fix i
       assume i: "i \<in> ?M" 
       from step[of i, unfolded step_def] have *: "I i < ?n" "K i < ?n" 
         and id: "bs ! K i = as ! J i" and decr: "decr (J i) (I i)" by auto
       from decr[unfolded decr_def] only_NS[OF i] have "J i = I i" by auto
       with id have id: "bs ! K i = as ! I i" by auto
       note only_NS[OF i] id
     } note pre_result = this
     {
       fix i
       assume i: "i \<in> ?M" 
       have *: "I i < ?m" "K i < ?m" 
       proof (rule pre_result[OF i])
         have "\<exists> j \<in> ?M. K i = I j" 
         proof (cases "Suc i \<in> ?M")
           case True
           show ?thesis by (rule bexI[OF _ True], auto simp: K_def I_def)
         next
           case False
           with i have id: "n + m = Suc i" by auto
           hence id: "K i = I m" by (subst Im[symmetric], unfold id, auto simp: K_def I_def) 
           with i show ?thesis by (intro bexI[of _ m], auto simp: K_def I_def)
         qed
         with pre_result show "K i < ?m" by auto
       qed
       from pre_result(2)[OF i] * l1 have "bs1 ! K i = as1 ! I i" "K i = I (Suc i)" 
         unfolding as_def bs_def by (auto simp: nth_append K_def I_def)
       with * have "bs1 ! I (Suc i) = as1 ! I i" "I i < ?m" "I (Suc i) < ?m" 
         by auto
     } note pre_identities = this
     define M where "M = ?M" 
     note inj = inj[folded M_def]
     define nxt where "nxt i = (if Suc i = n + m then m else Suc i)" for i
     define prv where "prv i = (if i = m then n + m - 1 else i - 1)" for i
     {
       fix i
       assume "i \<in> M" 
       hence i: "i \<in> ?M" unfolding M_def by auto
       from i n have inM: "nxt i \<in> M" "prv i \<in> M" "nxt (prv i) = i" "prv (nxt i) = i"
         unfolding nxt_def prv_def by (auto simp: M_def)
       from i pre_identities[OF i] pre_identities[of m] Im n
       have nxt: "bs1 ! I (nxt i) = as1 ! I i"  
         unfolding nxt_def prv_def by (auto simp: M_def)
       note nxt inM
     } note identities = this
   
   
     (* next up: remove elements indexed by I ` ?m from both as1 and bs1 
        and apply induction hypothesis *)
     note identities = identities[folded M_def]
     define Drop where "Drop = I ` M" 
 
     define rem_idx where "rem_idx = filter (\<lambda> i. i \<notin> Drop) [0..<?m]" 
     define drop_idx where "drop_idx = filter (\<lambda> i. i \<in> Drop) [0..<?m]" 
     define as1' where "as1' = map ((!) as1) rem_idx" 
     define bs1' where "bs1' = map ((!) bs1) rem_idx"
     define as1'' where "as1'' = map ((!) as1) drop_idx" 
     define bs1'' where "bs1'' = map ((!) bs1) drop_idx" 
     {
       fix as1 :: "'a list" and D :: "nat set" 
       define I where "I = [0..< length as1]" 
       have "mset as1 = mset (map ((!) as1) I)" unfolding I_def
         by (rule arg_cong[of _ _ mset], intro nth_equalityI, auto)
       also have "\<dots> = mset (map ((!) as1) (filter (\<lambda> i. i \<in> D) I))
           + mset (map ((!) as1) (filter (\<lambda> i. i \<notin> D) I))" 
         by (induct I, auto)
       also have "I = [0..< length as1]" by fact
       finally have "mset as1 = mset (map ((!) as1) (filter (\<lambda>i. i \<in> D) [0..<length as1])) + mset (map ((!) as1) (filter (\<lambda>i. i \<notin> D) [0..<length as1]))" .
     } note split = this
     from split[of bs1 Drop, folded rem_idx_def drop_idx_def, folded bs1'_def bs1''_def]
     have bs1: "mset bs1 = mset bs1'' + mset bs1'" .
     from split[of as1 Drop, unfolded l1, folded rem_idx_def drop_idx_def, folded as1'_def as1''_def]
     have as1: "mset as1 = mset as1'' + mset as1'" .
 
     (* showing that as1'' = bs1'' *)
     define I' where "I' = the_inv_into M I" 
     have bij: "bij_betw I M Drop" using inj unfolding Drop_def by (rule inj_on_imp_bij_betw)
     from the_inv_into_f_f[OF inj, folded I'_def] have I'I: "i \<in> M \<Longrightarrow> I' (I i) = i" for i by auto
     from bij I'I have II': "i \<in> Drop \<Longrightarrow> I (I' i) = i" for i
       by (simp add: I'_def f_the_inv_into_f_bij_betw)
     from II' I'I identities bij have Drop_M: "i \<in> Drop \<Longrightarrow> I' i \<in> M" for i
       using Drop_def by force
     have M_Drop: "i \<in> M \<Longrightarrow> I i \<in> Drop" for i unfolding Drop_def by auto
     {
       fix x
       assume "x \<in> Drop" 
       then obtain i where i: "i \<in> M" and x: "x = I i" unfolding Drop_def by auto
       have "x < ?m" unfolding x using i pre_identities[of i] unfolding M_def by auto
     } note Drop_m = this
     hence drop_idx: "set drop_idx = Drop" unfolding M_def drop_idx_def set_filter set_upt by auto
     have "mset as1'' = mset (map ((!) as1) drop_idx)" unfolding as1''_def mset_map by auto
     also have "drop_idx = map (I o I') drop_idx" using drop_idx by (intro nth_equalityI, auto intro!: II'[symmetric])
     also have "map ((!) as1) \<dots> = map (\<lambda> i. as1 ! I i) (map I' drop_idx)" by auto
     also have "\<dots> = map (\<lambda> i. bs1 ! I (nxt i)) (map I' drop_idx)" 
       by (rule map_cong[OF refl], rule identities(1)[symmetric], insert drop_idx Drop_M, auto)
     also have "\<dots> = map ((!) bs1) (map (I o nxt o I') drop_idx)" 
       by auto
     also have "mset \<dots> = image_mset ((!) bs1) (image_mset (I o nxt o I') (mset drop_idx))" unfolding mset_map ..
     also have "image_mset (I o nxt o I') (mset drop_idx) = image_mset I (image_mset nxt (image_mset I' (mset drop_idx)))" 
       by (metis multiset.map_comp)
     also have "image_mset nxt (image_mset I' (mset drop_idx)) = image_mset I' (mset drop_idx)" 
     proof -
       have dist: "distinct drop_idx" unfolding drop_idx_def by auto
       have injI': "inj_on I' Drop" using II' by (rule inj_on_inverseI)
       have "mset drop_idx = mset_set Drop" unfolding drop_idx[symmetric]
         by (rule mset_set_set[symmetric, OF dist])
       from image_mset_mset_set[OF injI', folded this]
       have "image_mset I' (mset drop_idx) = mset_set (I' ` Drop)" by auto
       also have "I' ` Drop = M" using II' I'I M_Drop Drop_M by force
       finally have id: "image_mset I' (mset drop_idx) = mset_set M" .
       have inj_nxt: "inj_on nxt M" using identities by (intro inj_on_inverseI)
       have nxt: "nxt ` M = M" using identities by force
       show ?thesis unfolding id image_mset_mset_set[OF inj_nxt] nxt ..
     qed
     also have "image_mset I \<dots> = mset drop_idx" unfolding multiset.map_comp using II' 
       by (intro multiset.map_ident_strong, auto simp: drop_idx)
     also have "image_mset ((!) bs1) \<dots> = mset bs1''" unfolding bs1''_def mset_map ..
     finally have bs1'': "mset bs1'' = mset as1''" ..
 
     (* showing the remaining identities *)
     let ?A = "mset as1' + mset as2" 
     let ?B = "mset bs1' + mset bs2" 
     from as1 bs1'' have as1: "mset as1 = mset bs1'' + mset as1'" by auto
     have A: "A = mset bs1'' + ?A" unfolding A A1 A2 as1 by auto
     have B: "A = mset bs1'' + ?B" unfolding B B1 B2 bs1 by auto
     from A[unfolded B] have AB: "?A = ?B" by simp
     
     have l1': "length as1' = length bs1'" unfolding as1'_def bs1'_def by auto
     have NS: "(mset as1', mset bs1') \<in> multpw NS" 
     proof (rule multpw_listI[OF l1' refl refl], intro allI impI)
       fix i
       assume i: "i < length bs1'"
       hence "rem_idx ! i \<in> set rem_idx" unfolding bs1'_def by (auto simp: nth_append)
       hence ri: "rem_idx ! i < ?m" unfolding rem_idx_def by auto
       from NSS[OF this] i
       show "(as1' ! i, bs1' ! i) \<in> NS" unfolding as1'_def bs1'_def by (auto simp: nth_append)
     qed
     have S: "(mset as1' + mset as2, ?B) \<in> s_mul_ext NS S"
       by (intro s_mul_extI[OF refl refl NS], unfold A2[symmetric] B2[symmetric], rule ne, rule S)
     have irr: "irrefl_on (set_mset ?B) S" using 1(2) B unfolding irrefl_on_def by simp
     have "M \<noteq> {}" unfolding M_def using n by auto
     hence "Drop \<noteq> {}" unfolding Drop_def by auto
     with drop_idx have "drop_idx \<noteq> []" by auto
     hence "bs1'' \<noteq> []" unfolding bs1''_def by auto
     hence "?B \<subset># A" unfolding B by (simp add: subset_mset.less_le)
     hence "size ?B < size A" by (rule mset_subset_size)
     thus False using 1(1) AB S irr by auto
   qed
 qed
   
 lemma mul_ext_irrefl: assumes "\<And> x. x \<in> set xs \<Longrightarrow> \<not> fst (rel x x)" 
   and "\<And> x y z. fst (rel x y) \<Longrightarrow> snd (rel y z) \<Longrightarrow> fst (rel x z)"
   and "\<And> x y. fst (rel x y) \<Longrightarrow> snd (rel x y)" 
 shows "\<not> fst (mul_ext rel xs xs)" 
   unfolding mul_ext_def Let_def fst_conv
   by (rule s_mul_ext_irrefl, insert assms, auto simp: irrefl_on_def)
 
 text \<open>The non-strict order is transitive.\<close>
 
 lemma ns_mul_ext_trans:
   assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
     and "(A, B) \<in> ns_mul_ext ns s"
     and "(B, C) \<in> ns_mul_ext ns s"
   shows "(A, C) \<in> ns_mul_ext ns s"
   using assms unfolding compatible_l_def compatible_r_def ns_mul_ext_def
   using trans_mult2_ns[of "s\<inverse>" "ns\<inverse>"]
   by (auto simp: mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric]) (metis trans_def)
 
 text\<open>The strict order is trans.\<close>
 
 lemma s_mul_ext_trans:
   assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
     and "(A, B) \<in> s_mul_ext ns s"
     and "(B, C) \<in> s_mul_ext ns s"
   shows "(A, C) \<in> s_mul_ext ns s"
   using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def
   using trans_mult2_s[of "s\<inverse>" "ns\<inverse>"]
   by (auto simp: mult2_s_eq_mult2_s_alt converse_relcomp[symmetric]) (metis trans_def)
 
 text\<open>The strict order is compatible on the left with the non strict one\<close>
 
 lemma s_ns_mul_ext_trans:
   assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
     and "(A, B) \<in> s_mul_ext ns s"
     and "(B, C) \<in> ns_mul_ext ns s"
   shows "(A, C) \<in> s_mul_ext ns s"
   using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def ns_mul_ext_def
   using compat_mult2(1)[of "s\<inverse>" "ns\<inverse>"]
   by (auto simp: mult2_s_eq_mult2_s_alt mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric])
 
 
 text\<open>The strict order is compatible on the right with the non-strict one.\<close>
 
 lemma ns_s_mul_ext_trans:
   assumes "trans s" "trans ns" "compatible_l ns s" "compatible_r ns s" "refl ns"
     and "(A, B) \<in> ns_mul_ext ns s"
     and "(B, C) \<in> s_mul_ext ns s"
   shows "(A, C) \<in> s_mul_ext ns s"
   using assms unfolding compatible_l_def compatible_r_def s_mul_ext_def ns_mul_ext_def
   using compat_mult2(2)[of "s\<inverse>" "ns\<inverse>"]
   by (auto simp: mult2_s_eq_mult2_s_alt mult2_ns_eq_mult2_ns_alt converse_relcomp[symmetric])
 
 text\<open>@{const s_mul_ext} is strongly normalizing\<close>
 
 lemma SN_s_mul_ext_strong:
   assumes "order_pair s ns"
     and "\<forall>y. y \<in># M \<longrightarrow> SN_on s {y}"
   shows "SN_on (s_mul_ext ns s) {M}"
   using mult2_s_eq_mult2_s_alt[of "ns\<inverse>" "s\<inverse>"] assms wf_below_pointwise[of "s\<inverse>" "set_mset M"]
   unfolding SN_on_iff_wf_below s_mul_ext_def order_pair_def compat_pair_def pre_order_pair_def
   by (auto intro!: wf_below_mult2_s_local simp: converse_relcomp[symmetric])
 
 lemma SN_s_mul_ext:
   assumes "order_pair s ns" "SN s"
   shows "SN (s_mul_ext ns s)"
   using SN_s_mul_ext_strong[OF assms(1)] assms(2)
   by (auto simp: SN_on_def)
 
 lemma (in order_pair) mul_ext_order_pair:
   "order_pair (s_mul_ext NS S) (ns_mul_ext NS S)" (is "order_pair ?S ?NS")
 proof
   from s_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
   show "trans ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
 next
   from ns_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
   show "trans ?NS" unfolding trans_def compatible_l_def compatible_r_def by blast
 next
   from ns_s_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
   show "?NS O ?S \<subseteq> ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
 next
   from s_ns_mul_ext_trans trans_S trans_NS compat_NS_S compat_S_NS refl_NS
   show "?S O ?NS \<subseteq> ?S" unfolding trans_def compatible_l_def compatible_r_def by blast
 next
   from ns_mul_ext_refl[OF refl_NS, of _ S]
   show "refl ?NS" unfolding refl_on_def by fast
 qed
 
 lemma (in SN_order_pair) mul_ext_SN_order_pair: "SN_order_pair (s_mul_ext NS S) (ns_mul_ext NS S)"
   (is "SN_order_pair ?S ?NS")
 proof -
   from mul_ext_order_pair
   interpret order_pair ?S ?NS .
   have "order_pair S NS" by unfold_locales
   then interpret SN_ars ?S using SN_s_mul_ext[of S NS] SN by unfold_locales
   show ?thesis by unfold_locales
 qed
 
 lemma mul_ext_compat:
   assumes compat: "\<And> s t u. \<lbrakk>s \<in> set ss; t \<in> set ts; u \<in> set us\<rbrakk> \<Longrightarrow>
     (snd (f s t) \<and> fst (f t u) \<longrightarrow> fst (f s u)) \<and>
     (fst (f s t) \<and> snd (f t u) \<longrightarrow> fst (f s u)) \<and>
     (snd (f s t) \<and> snd (f t u) \<longrightarrow> snd (f s u)) \<and>
     (fst (f s t) \<and> fst (f t u) \<longrightarrow> fst (f s u))"
   shows "
     (snd (mul_ext f ss ts) \<and> fst (mul_ext f ts us) \<longrightarrow> fst (mul_ext f ss us)) \<and>
     (fst (mul_ext f ss ts) \<and> snd (mul_ext f ts us) \<longrightarrow> fst (mul_ext f ss us)) \<and>
     (snd (mul_ext f ss ts) \<and> snd (mul_ext f ts us) \<longrightarrow> snd (mul_ext f ss us)) \<and>
     (fst (mul_ext f ss ts) \<and> fst (mul_ext f ts us) \<longrightarrow> fst (mul_ext f ss us)) "
 proof -
   let ?s = "{(x, y). fst (f x y)}\<inverse>" and ?ns = "{(x, y). snd (f x y)}\<inverse>"
   have [dest]: "(mset ts, mset ss) \<in> mult2_alt b2 ?ns ?s \<Longrightarrow> (mset us, mset ts) \<in> mult2_alt b1 ?ns ?s \<Longrightarrow>
     (mset us, mset ss) \<in> mult2_alt (b1 \<and> b2) ?ns ?s" for b1 b2
     using assms by (auto intro!: trans_mult2_alt_local[of _ "mset ts"] simp: in_multiset_in_set)
   show ?thesis by (auto simp: mul_ext_def s_mul_ext_def ns_mul_ext_def Let_def)
 qed
 
 lemma mul_ext_cong[fundef_cong]:
   assumes "mset xs1 = mset ys1"
     and "mset xs2 = mset ys2"
     and "\<And> x x'. x \<in> set ys1 \<Longrightarrow> x' \<in> set ys2 \<Longrightarrow> f x x' = g x x'"
   shows "mul_ext f xs1 xs2 = mul_ext g ys1 ys2"
   using assms
     mult2_alt_map[of "mset xs2" "mset xs1" "{(x, y). snd (f x y)}\<inverse>" id id "{(x, y). snd (g x y)}\<inverse>"
       "{(x, y). fst (f x y)}\<inverse>" "{(x, y). fst (g x y)}\<inverse>"]
     mult2_alt_map[of "mset ys2" "mset ys1" "{(x, y). snd (g x y)}\<inverse>" id id "{(x, y). snd (f x y)}\<inverse>"
       "{(x, y). fst (g x y)}\<inverse>" "{(x, y). fst (f x y)}\<inverse>"]
   by (auto simp: mul_ext_def s_mul_ext_def ns_mul_ext_def Let_def in_multiset_in_set)
 
 lemma all_nstri_imp_mul_nstri:
   assumes "\<forall>i<length ys. snd (f (xs ! i) (ys ! i))"
     and "length xs = length ys"
   shows "snd (mul_ext f xs ys)"
 proof-
   from assms(1) have "\<forall>i. i < length ys \<longrightarrow> (xs ! i, ys ! i) \<in> {(x,y). snd (f x y)}" by simp
   from all_ns_ns_mul_ext[OF assms(2) this] show ?thesis by (simp add: mul_ext_def)
 qed
 
 lemma relation_inter:
   shows "{(x,y). P x y} \<inter> {(x,y). Q x y} = {(x,y). P x y \<and> Q x y}"
   by blast
 
 lemma mul_ext_unfold:
   "(x,y) \<in> {(a,b). fst (mul_ext g a b)} \<longleftrightarrow> (mset x, mset y) \<in> (s_mul_ext {(a,b). snd (g a b)} {(a,b). fst (g a b)})"
   unfolding mul_ext_def by (simp add: Let_def)
 
 text \<open>The next lemma is a local version of strong-normalization of
   the multiset extension, where the base-order only has to be strongly normalizing
   on elements of the multisets. This will be crucial for orders that are defined recursively
   on terms, such as RPO or WPO.\<close>
 lemma mul_ext_SN:
   assumes "\<forall>x. snd (g x x)"
     and "\<forall>x y z. fst (g x y) \<longrightarrow> snd (g y z) \<longrightarrow> fst (g x z)"
     and "\<forall>x y z. snd (g x y) \<longrightarrow> fst (g y z) \<longrightarrow> fst (g x z)"
     and "\<forall>x y z. snd (g x y) \<longrightarrow> snd (g y z) \<longrightarrow> snd (g x z)"
     and "\<forall>x y z. fst (g x y) \<longrightarrow> fst (g y z) \<longrightarrow> fst (g x z)"
   shows "SN {(ys, xs).
   (\<forall>y\<in>set ys. SN_on {(s ,t). fst (g s t)} {y}) \<and>
   fst (mul_ext g ys xs)}"
 proof -
   let ?R1 = "\<lambda>xs ys. \<forall>y\<in> set ys. SN_on {(s ,t). fst (g s t)} {y}"
   let ?R2 = "\<lambda>xs ys. fst (mul_ext g ys xs)"
   let ?s = "{(x,y). fst (g x y)}" and ?ns = "{(x,y). snd (g x y)}"
   have OP: "order_pair ?s ?ns" using assms(1-5)
     by unfold_locales ((unfold refl_on_def trans_def)?, blast)+
   let ?R = "{(ys, xs). ?R1 xs ys \<and> ?R2 xs ys}"
   let ?Sn = "SN_on ?R"
   {
     fix ys xs
     assume R_ys_xs: "(ys, xs) \<in> ?R"
     let ?mys = "mset ys"
     let ?mxs = "mset xs"
     from R_ys_xs have  HSN_ys: "\<forall>y. y \<in> set ys \<longrightarrow> SN_on ?s {y}" by simp
     with in_multiset_in_set[of ys] have "\<forall>y. y \<in># ?mys \<longrightarrow> SN_on ?s {y}" by simp
     from SN_s_mul_ext_strong[OF OP this] and mul_ext_unfold
     have "SN_on {(ys,xs). fst (mul_ext g ys xs)} {ys}" by fast
     from relation_inter[of ?R2 ?R1] and SN_on_weakening[OF this]
     have "SN_on ?R {ys}" by blast
   }
   then have Hyp: "\<forall>ys xs. (ys,xs) \<in> ?R \<longrightarrow> SN_on ?R {ys}" by auto
   {
     fix ys
     have "SN_on ?R {ys}"
     proof (cases "\<exists> xs. (ys, xs) \<in> ?R")
       case True with Hyp show ?thesis by simp
     next
       case False then show ?thesis by auto
     qed
   }
   then show ?thesis unfolding SN_on_def by simp
 qed
 
 lemma mul_ext_stri_imp_nstri:
   assumes "fst (mul_ext f as bs)"
   shows "snd (mul_ext f as bs)"
   using assms and s_ns_mul_ext unfolding mul_ext_def by (auto simp: Let_def)
 
 lemma ns_ns_mul_ext_union_compat:
   assumes "(A,B) \<in> ns_mul_ext ns s"
     and "(C,D) \<in> ns_mul_ext ns s"
   shows "(A + C, B + D) \<in> ns_mul_ext ns s"
   using assms by (auto simp: ns_mul_ext_def intro: mult2_alt_ns_ns_add)
 
 lemma s_ns_mul_ext_union_compat:
   assumes "(A,B) \<in> s_mul_ext ns s"
     and "(C,D) \<in> ns_mul_ext ns s"
   shows "(A + C, B + D) \<in> s_mul_ext ns s"
   using assms by (auto simp: s_mul_ext_def ns_mul_ext_def intro: mult2_alt_s_ns_add)
 
 lemma ns_ns_mul_ext_union_compat_rtrancl: assumes refl: "refl ns"
   and AB: "(A, B) \<in> (ns_mul_ext ns s)\<^sup>*"
   and CD: "(C, D) \<in> (ns_mul_ext ns s)\<^sup>*"
 shows "(A + C, B + D) \<in> (ns_mul_ext ns s)\<^sup>*"
 proof -
   {
     fix A B C
     assume "(A, B) \<in> (ns_mul_ext ns s)\<^sup>*"
     then have "(A + C, B + C) \<in> (ns_mul_ext ns s)\<^sup>*"
     proof (induct rule: rtrancl_induct)
       case (step B D)
       have "(C, C) \<in> ns_mul_ext ns s"
         by (rule ns_mul_ext_refl, insert refl, auto simp: locally_refl_def refl_on_def)
       from ns_ns_mul_ext_union_compat[OF step(2) this] step(3)
       show ?case by auto
     qed auto
   }
   from this[OF AB, of C] this[OF CD, of B]
   show ?thesis by (auto simp: ac_simps)
 qed
 
 subsection \<open>Multisets as order on lists\<close>
 
 interpretation mul_ext_list: list_order_extension
   "\<lambda>s ns. {(as, bs). (mset as, mset bs) \<in> s_mul_ext ns s}"
   "\<lambda>s ns. {(as, bs). (mset as, mset bs) \<in> ns_mul_ext ns s}"
 proof -
   let ?m = "mset :: ('a list \<Rightarrow> 'a multiset)"
   let ?S = "\<lambda>s ns. {(as, bs). (?m as, ?m bs) \<in> s_mul_ext ns s}"
   let ?NS = "\<lambda>s ns. {(as, bs). (?m as, ?m bs) \<in> ns_mul_ext ns s}"
   show "list_order_extension ?S ?NS"
   proof (rule list_order_extension.intro)
     fix s ns
     let ?s = "?S s ns"
     let ?ns = "?NS s ns"
     assume "SN_order_pair s ns"
     then interpret SN_order_pair s ns .
     interpret SN_order_pair "(s_mul_ext ns s)" "(ns_mul_ext ns s)"
       by (rule mul_ext_SN_order_pair)
     show "SN_order_pair ?s ?ns"
     proof
       show "refl ?ns" using refl_NS unfolding refl_on_def by blast
       show "?ns O ?s \<subseteq> ?s" using compat_NS_S by blast
       show "?s O ?ns \<subseteq> ?s" using compat_S_NS by blast
       show "trans ?ns" using trans_NS unfolding trans_def by blast
       show "trans ?s" using trans_S unfolding trans_def by blast
       show "SN ?s" using SN_inv_image[OF SN, of ?m, unfolded inv_image_def] .
     qed
   next
     fix S f NS as bs
     assume "\<And>a b. (a, b) \<in> S \<Longrightarrow> (f a, f b) \<in> S"
       "\<And>a b. (a, b) \<in> NS \<Longrightarrow> (f a, f b) \<in> NS"
       "(as, bs) \<in> ?S S NS"
     then show "(map f as, map f bs) \<in> ?S S NS"
       using mult2_alt_map[of _ _ "NS\<inverse>" f f "NS\<inverse>" "S\<inverse>" "S\<inverse>"] by (auto simp: mset_map s_mul_ext_def)
   next
     fix S f NS as bs
     assume "\<And>a b. (a, b) \<in> S \<Longrightarrow> (f a, f b) \<in> S"
       "\<And>a b. (a, b) \<in> NS \<Longrightarrow> (f a, f b) \<in> NS"
       "(as, bs) \<in> ?NS S NS"
     then show "(map f as, map f bs) \<in> ?NS S NS"
       using mult2_alt_map[of _ _ "NS\<inverse>" f f "NS\<inverse>" "S\<inverse>" "S\<inverse>"] by (auto simp: mset_map ns_mul_ext_def)
   next
     fix as bs :: "'a list" and NS S :: "'a rel"
     assume ass: "length as = length bs"
       "\<And>i. i < length bs \<Longrightarrow> (as ! i, bs ! i) \<in> NS"
     show "(as, bs) \<in> ?NS S NS"
       by (rule, unfold split, rule all_ns_ns_mul_ext, insert ass, auto)
   qed
 qed
 
 lemma s_mul_ext_singleton [simp, intro]:
   assumes "(a, b) \<in> s"
   shows "({#a#}, {#b#}) \<in> s_mul_ext ns s"
   using assms by (auto simp: s_mul_ext_def mult2_alt_s_single)
 
 lemma ns_mul_ext_singleton [simp, intro]:
   "(a, b) \<in> ns \<Longrightarrow> ({#a#}, {#b#}) \<in> ns_mul_ext ns s"
   by (auto simp: ns_mul_ext_def multpw_converse intro: multpw_implies_mult2_alt_ns multpw_single)
 
 lemma ns_mul_ext_singleton2:
   "(a, b) \<in> s \<Longrightarrow> ({#a#}, {#b#}) \<in> ns_mul_ext ns s"
   by (intro s_ns_mul_ext s_mul_ext_singleton)
 
 lemma s_mul_ext_self_extend_left:
   assumes "A \<noteq> {#}" and "locally_refl W B"
   shows "(A + B, B) \<in> s_mul_ext W S"
 proof -
   have "(A + B, {#} + B) \<in> s_mul_ext W S"
     using assms by (intro s_mul_ext_union_compat) (auto dest: s_mul_ext_bottom)
   then show ?thesis by simp
 qed
 
 lemma s_mul_ext_ne_extend_left:
   assumes "A \<noteq> {#}" and "(B, C) \<in> ns_mul_ext W S"
   shows "(A + B, C) \<in> s_mul_ext W S"
   using assms
 proof -
   have "(A + B, {#} + C) \<in> s_mul_ext W S"
     using assms by (intro s_ns_mul_ext_union_compat)
       (auto simp: s_mul_ext_bottom dest: s_ns_mul_ext)
   then show ?thesis by (simp add: ac_simps)
 qed
 
 lemma s_mul_ext_extend_left:
   assumes "(B, C) \<in> s_mul_ext W S"
   shows "(A + B, C) \<in> s_mul_ext W S"
   using assms
 proof -
   have "(B + A, C + {#}) \<in> s_mul_ext W S"
     using assms by (intro s_ns_mul_ext_union_compat)
       (auto simp: ns_mul_ext_bottom dest: s_ns_mul_ext)
   then show ?thesis by (simp add: ac_simps)
 qed
 
 lemma mul_ext_mono:
   assumes "\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys; fst (P x y)\<rbrakk> \<Longrightarrow> fst (P' x y)"
     and   "\<And>x y. \<lbrakk>x \<in> set xs; y \<in> set ys; snd (P x y)\<rbrakk> \<Longrightarrow> snd (P' x y)"
   shows
     "fst (mul_ext P xs ys) \<Longrightarrow> fst (mul_ext P' xs ys)"
     "snd (mul_ext P xs ys) \<Longrightarrow> snd (mul_ext P' xs ys)"
   unfolding mul_ext_def Let_def fst_conv snd_conv
 proof -
   assume mem: "(mset xs, mset ys) \<in> s_mul_ext {(x, y). snd (P x y)} {(x, y). fst (P x y)}"
   show "(mset xs, mset ys) \<in> s_mul_ext {(x, y). snd (P' x y)} {(x, y). fst (P' x y)}"
     by (rule s_mul_ext_local_mono[OF _ _ mem], insert assms, auto)
 next
   assume mem: "(mset xs, mset ys) \<in> ns_mul_ext {(x, y). snd (P x y)} {(x, y). fst (P x y)}"
   show "(mset xs, mset ys) \<in> ns_mul_ext {(x, y). snd (P' x y)} {(x, y). fst (P' x y)}"
     by (rule ns_mul_ext_local_mono[OF _ _ mem], insert assms, auto)
 qed
 
 
 
 subsection \<open>Special case: non-strict order is equality\<close>
 
 lemma ns_mul_ext_IdE:
   assumes "(M, N) \<in> ns_mul_ext Id R"
   obtains X and Y and Z where "M = X + Z" and "N = Y + Z"
     and "\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. (x, y) \<in> R"
   using assms
   by (auto simp: ns_mul_ext_def elim!: mult2_alt_nsE) (insert union_commute, blast)
 
 lemma ns_mul_ext_IdI:
   assumes "M = X + Z" and "N = Y + Z" and "\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. (x, y) \<in> R"
   shows "(M, N) \<in> ns_mul_ext Id R"
   using assms mult2_alt_nsI[of N Z Y M Z X Id "R\<inverse>"]
   by (auto simp: ns_mul_ext_def)
 
 lemma s_mul_ext_IdE:
   assumes "(M, N) \<in> s_mul_ext Id R"
   obtains X and Y and Z where "X \<noteq> {#}" and "M = X + Z" and "N = Y + Z"
     and "\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. (x, y) \<in> R"
   using assms
   by (auto simp: s_mul_ext_def elim!: mult2_alt_sE) (metis union_commute)
 
 lemma s_mul_ext_IdI:
   assumes "X \<noteq> {#}" and "M = X + Z" and "N = Y + Z"
     and "\<forall>y \<in> set_mset Y. \<exists>x \<in> set_mset X. (x, y) \<in> R"
   shows "(M, N) \<in> s_mul_ext Id R"
   using assms mult2_alt_sI[of N Z Y M Z X Id "R\<inverse>"]
   by (auto simp: s_mul_ext_def ac_simps)
 
 lemma mult_s_mul_ext_conv:
   assumes "trans R"
   shows "(mult (R\<inverse>))\<inverse> = s_mul_ext Id R"
   using mult2_s_eq_mult2_s_alt[of Id "R\<inverse>"] assms
   by (auto simp: s_mul_ext_def refl_Id mult2_s_def)
 
 lemma ns_mul_ext_Id_eq:
   "ns_mul_ext Id R = (s_mul_ext Id R)\<^sup>="
   by (auto simp add: ns_mul_ext_def s_mul_ext_def mult2_alt_ns_conv)
 
 lemma subseteq_mset_imp_ns_mul_ext_Id:
   assumes "A \<subseteq># B"
   shows "(B, A) \<in> ns_mul_ext Id R"
 proof -
   obtain C where [simp]: "B = C + A" using assms by (auto simp: mset_subset_eq_exists_conv ac_simps)
   have "(C + A, {#} + A) \<in> ns_mul_ext Id R"
     by (intro ns_mul_ext_IdI [of _ C A _ "{#}"]) auto
   then show ?thesis by simp
 qed
 
 lemma subset_mset_imp_s_mul_ext_Id:
   assumes "A \<subset># B"
   shows "(B, A) \<in> s_mul_ext Id R"
   using assms by (intro supset_imp_s_mul_ext) (auto simp: refl_Id)
 
 
 end