Theory Multiset_Extension_Pair

section ‹Multiset extension of an order pair›

text ‹Given a well-founded order $\prec$ and a compatible non-strict order $\precsim$,
  we define the corresponding multiset-extension of these orders.›

theory Multiset_Extension_Pair
  imports 
    "HOL-Library.Multiset" 
    "Regular-Sets.Regexp_Method"
    "Abstract-Rewriting.Abstract_Rewriting" 
    Relations
begin

(* Possible to generalize by assuming trans locally *)

lemma mult_locally_cancel:
  assumes "trans s " and "locally_irrefl s (X + Z)" and "locally_irrefl s (Y + Z)"
  shows "(X + Z, Y + Z)  mult s  (X, Y)  mult s" (is "?L  ?R")
proof
  assume ?L thus ?R using assms(2, 3)
  proof (induct Z arbitrary: X Y)
    case (add z Z)
    obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y'  {#}"
      "x  set_mset X'. y  set_mset Y'. (x, y)  s"
      using mult_implies_one_step[OF trans s add(2)] by auto
    consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
      using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
    thus ?case
    proof (cases)
      case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2] 
        by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
          (metis add.hyps add.prems(2) add.prems(3) add_mset_add_single li_trans_l union_mset_add_mset_right) 
    next
      case 2 then obtain y where "y  set_mset Y2" "(z, y)  s" using *(4) add(3, 4)
        by (auto simp: locally_irrefl_def)
      moreover from this transD[OF trans s _ this(2)]
      have "x'  set_mset X2  y  set_mset Y2. (x', y)  s" for x'
        using 2 *(4)[rule_format, of x'] by auto
      ultimately show ?thesis using  * one_step_implies_mult[of Y2 X2 s Z'] 2 add(3, 4)
        by (force simp: locally_irrefl_def add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1))
    qed
  qed auto
next
  assume ?R then obtain I J K
    where "Y = I + J" "X = I + K" "J  {#}" "k  set_mset K. j  set_mset J. (k, j)  s"
    using mult_implies_one_step[OF trans s] by blast
  thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
qed

lemma mult_locally_cancelL:
  assumes "trans s" "locally_irrefl s (X + Z)" "locally_irrefl s (Y + Z)"
  shows "(Z + X, Z + Y)  mult s  (X, Y)  mult s"
  using mult_locally_cancel[OF assms] by (simp only: union_commute)

lemma mult_cancelL:
  assumes "trans s" "irrefl s" shows "(Z + X, Z + Y)  mult s  (X, Y)  mult s"
  using assms
  by (auto simp: union_commute intro!: mult_cancel elim: irrefl_on_subset) 

lemma wf_trancl_conv:
  shows "wf (r+)  wf r"
  using wf_subset[of "r+" r] by (force simp: wf_trancl)

subsection ‹Pointwise multiset order›

inductive_set multpw :: "'a rel  'a multiset rel" for ns :: "'a rel" where
  empty: "({#}, {#})  multpw ns"
| add: "(x, y)  ns  (X, Y)  multpw ns  (add_mset x X, add_mset y Y)  multpw ns"

lemma multpw_emptyL [simp]:
  "({#}, X)  multpw ns  X = {#}"
  by (cases X) (auto elim: multpw.cases intro: multpw.intros)

lemma multpw_emptyR [simp]:
  "(X, {#})  multpw ns  X = {#}"
  by (cases X) (auto elim: multpw.cases intro: multpw.intros)

lemma refl_multpw:
  assumes "refl ns" shows "refl (multpw ns)"
proof -
  have "(X, X)  multpw ns" for X using assms
    by (induct X) (auto intro: multpw.intros simp: refl_on_def)
  then show ?thesis by (auto simp: refl_on_def)
qed

lemma multpw_Id_Id [simp]:
  "multpw Id = Id"
proof -
  have "(X, Y)  multpw (Id :: 'a rel)  X = Y" for X Y by (induct X Y rule: multpw.induct) auto
  then show ?thesis using refl_multpw[of Id] by (auto simp: refl_on_def)
qed

lemma mono_multpw:
  assumes "ns  ns'" shows "multpw ns  multpw ns'"
proof -
  have "(X, Y)  multpw ns  (X, Y)  multpw ns'" for X Y
    by (induct X Y rule: multpw.induct) (insert assms, auto intro: multpw.intros)
  then show ?thesis by auto
qed

lemma multpw_converse:
  "multpw (ns¯) = (multpw ns)¯"
proof -
  have "(X, Y)  multpw (ns¯)  (X, Y)  (multpw ns)¯" for X Y and ns :: "'a rel"
    by (induct X Y rule: multpw.induct) (auto intro: multpw.intros)
  then show ?thesis by auto
qed

lemma multpw_local:
  "(X, Y)  multpw ns  (X, Y)  multpw (ns  set_mset X × set_mset Y)"
proof (induct X Y rule: multpw.induct)
  case (add x y X Y) then show ?case
    using mono_multpw[of "ns  set_mset X × set_mset Y" "ns  insert x (set_mset X) × insert y (set_mset Y)"]
    by (auto intro: multpw.intros)
qed auto

lemma multpw_split1R:
  assumes "(add_mset x X, Y)  multpw ns"
  obtains z Z where "Y = add_mset z Z" and "(x, z)  ns" and "(X, Z)  multpw ns"
  using assms
proof (induct  "add_mset x X" Y arbitrary: X thesis rule: multpw.induct)
  case (add x' y' X' Y') then show ?case
  proof (cases "x = x'")
    case False
    obtain X'' where [simp]: "X = add_mset x' X''"
      using add(4) False
      by (metis add_eq_conv_diff)
    have "X' = add_mset x X''" using add(4) by (auto simp: add_eq_conv_ex)
    with add(2) obtain Y'' y where "Y' = add_mset y Y''" "(x,y)  ns" "(X'', Y'')  multpw ns"
      by (auto intro: add(3))
    then show ?thesis using add(1) add(5)[of y "add_mset y' Y''"]
      by (auto simp: ac_simps intro: multpw.intros)
  qed auto
qed auto

lemma multpw_splitR:
  assumes "(X1 + X2, Y)  multpw ns"
  obtains Y1 Y2 where "Y = Y1 + Y2" and "(X1, Y1)  multpw ns" and "(X2, Y2)  multpw ns"
  using assms
proof (induct X2 arbitrary: Y thesis)
  case (add x2 X2)
  from add(3) obtain Y' y2 where "(X1 + X2, Y')  multpw ns" "(x2, y2)  ns" "Y = add_mset y2 Y'"
    by (auto elim: multpw_split1R simp: union_assoc[symmetric])
  moreover then obtain Y1 Y2 where "(X1, Y1)  multpw ns" "(X2, Y2)  multpw ns" "Y' = Y1 + Y2"
    by (auto elim: add(1)[rotated])
  ultimately show ?case by (intro add(2)) (auto simp: union_assoc intro: multpw.intros)
qed auto

lemma multpw_split1L:
  assumes "(X, add_mset y Y)  multpw ns"
  obtains z Z where "X = add_mset z Z" and "(z, y)  ns" and "(Z, Y)  multpw ns"
  using assms multpw_split1R[of y Y X "ns¯" thesis] by (auto simp: multpw_converse)

lemma multpw_splitL:
  assumes "(X, Y1 + Y2)  multpw ns"
  obtains X1 X2 where "X = X1 + X2" and "(X1, Y1)  multpw ns" and "(X2, Y2)  multpw ns"
  using assms multpw_splitR[of Y1 Y2 X "ns¯" thesis] by (auto simp: multpw_converse)

lemma locally_trans_multpw:
  assumes "locally_trans ns S T U"
    and "(S, T)  multpw ns"
    and "(T, U)  multpw ns"
  shows "(S, U)  multpw ns"
  using assms(2,3,1)
proof (induct S T arbitrary: U rule: multpw.induct)
  case (add x y X Y)
  then show ?case unfolding locally_trans_def
    by (auto 0 3 intro: multpw.intros elim: multpw_split1R)
qed blast

lemma trans_multpw:
  assumes "trans ns" shows "trans (multpw ns)"
  using locally_trans_multpw unfolding locally_trans_def trans_def
  by (meson assms locally_trans_multpw tr_ltr)

lemma multpw_add:
  assumes "(X1, Y1)  multpw ns" "(X2, Y2)  multpw ns" shows "(X1 + X2, Y1 + Y2)  multpw ns"
  using assms(2,1)
  by (induct X2 Y2 rule: multpw.induct) (auto intro: multpw.intros simp: add.assoc[symmetric])

lemma multpw_single:
  "(x, y)  ns  ({#x#}, {#y#})  multpw ns"
  using multpw.intros(2)[OF _ multpw.intros(1)] .

lemma multpw_mult1_commute:
  assumes compat: "s O ns  s" and reflns: "refl ns"
  shows "mult1 s O multpw ns  multpw ns O mult1 s"
proof -
  { fix X Y Z assume 1: "(X, Y)  mult1 s" "(Y, Z)  multpw ns"
    then obtain X' Y' y where 2: "X = Y' + X'" "Y = add_mset y Y'" "x. x ∈# X'  (x, y)  s"
      by (auto simp: mult1_def)
    moreover obtain Z' z where 3: "Z = add_mset z Z'" "(y, z)  ns" "(Y', Z')  multpw ns"
      using 1(2) 2(2) by (auto elim: multpw_split1R)
    moreover have "x. x ∈# X'  (x, z)  s" using 2(3) 3(2) compat by blast
    ultimately have "Y'. (X, Y')  multpw ns  (Y', Z)  mult1 s" unfolding mult1_def
      using refl_multpw[OF reflns]
      by (intro exI[of _ "Z' + X'"]) (auto intro: multpw_add simp: refl_on_def)
  }
  then show ?thesis by fast
qed

lemma multpw_mult_commute:
  assumes "s O ns  s" "refl ns" shows "mult s O multpw ns  multpw ns O mult s"
proof -
  { fix X Y Z assume 1: "(X, Y)  mult s" "(Y, Z)  multpw ns"
    then have "Y'. (X, Y')  multpw ns  (Y', Z)  mult s" unfolding mult_def
      using multpw_mult1_commute[OF assms] by (induct rule: converse_trancl_induct) (auto 0 3)
  }
  then show ?thesis by fast
qed

lemma wf_mult_rel_multpw:
  assumes "wf s" "s O ns  s" "refl ns" shows "wf ((multpw ns)* O mult s O (multpw ns)*)"
  using assms(1) multpw_mult_commute[OF assms(2,3)] by (subst qc_wf_relto_iff) (auto simp: wf_mult)

lemma multpw_cancel1:
  assumes "trans ns" "(y, x)  ns"
  shows "(add_mset x X, add_mset y Y)  multpw ns  (X, Y)  multpw ns" (is "?L  ?R")
proof -
  assume ?L then obtain x' X' where X: "(x', y)  ns" "add_mset x' X' = add_mset x X" "(X', Y)  multpw ns"
    by (auto elim: multpw_split1L simp: union_assoc[symmetric])
  then show ?R
  proof (cases "x = x'")
    case False then obtain X2 where X2: "X' = add_mset x X2" "X = add_mset x' X2"
      using X(2) by (auto simp: add_eq_conv_ex)
    then obtain y' Y' where Y: "(x, y')  ns" "Y = add_mset y' Y'" "(X2, Y')  multpw ns"
      using X(3) by (auto elim: multpw_split1R)
    have "(x', y')  ns" using X(1) Y(1) trans ns assms(2) by (metis trans_def)
    then show ?thesis using Y by (auto intro: multpw.intros simp: X2)
  qed auto
qed

lemma multpw_cancel:
  assumes "refl ns" "trans ns"
  shows "(X + Z, Y + Z)  multpw ns  (X, Y)  multpw ns" (is "?L  ?R")
proof
  assume ?L then show ?R
  proof (induct Z)
    case (add z Z) then show ?case using multpw_cancel1[of ns z z "X + Z" "Y + Z"] assms
      by (auto simp: refl_on_def union_assoc)
  qed auto
next
  assume ?R then show ?L using assms refl_multpw by (auto intro: multpw_add simp: refl_on_def)
qed

lemma multpw_cancelL:
  assumes "refl ns" "trans ns" shows "(Z + X, Z + Y)  multpw ns  (X, Y)  multpw ns"
  using multpw_cancel[OF assms, of X Z Y] by (simp only: union_commute)

subsection ‹Multiset extension for order pairs via the pointwise order and @{const mult}

definition "mult2_s ns s  multpw ns O mult s"
definition "mult2_ns ns s  multpw ns O (mult s)="

lemma mult2_ns_conv:
  shows "mult2_ns ns s = mult2_s ns s  multpw ns"
  by (auto simp: mult2_s_def mult2_ns_def)

lemma mono_mult2_s:
  assumes "ns  ns'" "s  s'" shows "mult2_s ns s  mult2_s ns' s'"
  using mono_multpw[OF assms(1)] mono_mult[OF assms(2)] unfolding mult2_s_def by auto

lemma mono_mult2_ns:
  assumes "ns  ns'" "s  s'" shows "mult2_ns ns s  mult2_ns ns' s'"
  using mono_multpw[OF assms(1)] mono_mult[OF assms(2)] unfolding mult2_ns_def by auto

lemma wf_mult2_s:
  assumes "wf s" "s O ns  s" "refl ns"
  shows "wf (mult2_s ns s)"
  using wf_mult_rel_multpw[OF assms] assms by (auto simp: mult2_s_def wf_mult intro: wf_subset)

lemma refl_mult2_ns:
  assumes "refl ns" shows "refl (mult2_ns ns s)"
  using refl_multpw[OF assms] unfolding mult2_ns_def refl_on_def by fast

lemma trans_mult2_s:
  assumes "s O ns  s" "refl ns" "trans ns"
  shows "trans (mult2_s ns s)"
  using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
  unfolding mult2_s_def trans_O_iff by (blast 8)

lemma trans_mult2_ns:
  assumes "s O ns  s" "refl ns" "trans ns"
  shows "trans (mult2_ns ns s)"
  using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
  unfolding mult2_ns_def trans_O_iff by (blast 8)

lemma compat_mult2:
  assumes "s O ns  s" "refl ns" "trans ns"
  shows "mult2_ns ns s O mult2_s ns s  mult2_s ns s" "mult2_s ns s O mult2_ns ns s  mult2_s ns s"
  using trans_multpw[OF assms(3)] trans_trancl[of "mult1 s", folded mult_def] multpw_mult_commute[OF assms(1,2)]
  unfolding mult2_s_def mult2_ns_def trans_O_iff by (blast 8)+

text ‹Trivial inclusions›

lemma mult_implies_mult2_s:
  assumes "refl ns" "(X, Y)  mult s"
  shows "(X, Y)  mult2_s ns s"
  using refl_multpw[of ns] assms unfolding mult2_s_def refl_on_def by blast

lemma mult_implies_mult2_ns:
  assumes "refl ns" "(X, Y)  (mult s)="
  shows "(X, Y)  mult2_ns ns s"
  using refl_multpw[of ns] assms unfolding mult2_ns_def refl_on_def by blast

lemma multpw_implies_mult2_ns:
  assumes "(X, Y)  multpw ns"
  shows "(X, Y)  mult2_ns ns s"
  unfolding mult2_ns_def using assms by simp

subsection ‹One-step versions of the multiset extensions›

lemma mult2_s_one_step:
  assumes "ns O s  s" "refl ns" "trans s"
  shows "(X, Y)  mult2_s ns s  (X1 X2 Y1 Y2. X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw ns  Y2  {#}  (x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)))" (is "?L  ?R")
proof
  assume ?R then obtain X1 X2 Y1 Y2 where *: "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1)  multpw ns" and
    "Y2  {#}" "x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)" by blast
  then have "(Y1 + X2, Y1 + Y2)  mult s"
    using trans s by (auto intro: one_step_implies_mult)
  moreover have "(X1 + X2, Y1 + X2)  multpw ns"
    using refl ns refl_multpw[of ns] by (auto intro: multpw_add simp: refl_on_def *)
  ultimately show ?L by (auto simp: mult2_s_def *)
next
  assume ?L then obtain X1 X2 Z1 Z2 Y2 where *: "X = X1 + X2" "Y = Z1 + Y2" "(X1, Z1)  multpw ns"
    "(X2, Z2)  multpw ns" "Y2  {#}" "x. x ∈# Z2  (y. y ∈# Y2  (x, y)  s)"
    by (auto 0 3 dest!: mult_implies_one_step[OF trans s] simp: mult2_s_def elim!: multpw_splitL) metis
  have "x. x ∈# X2  (y. y ∈# Y2  (x,y)  s)"
  proof (intro allI impI)
    fix x assume "x ∈# X2"
    then obtain X2' where "X2 = add_mset x X2'" by (metis multi_member_split)
    then obtain z Z2' where "Z2 = add_mset z Z2'" "(x, z)  ns" using *(4) by (auto elim: multpw_split1R)
    then have "z ∈# Z2" "(x, z)  ns" by auto
    then show "y. y ∈# Y2  (x,y)  s" using *(6) ns O s  s by blast
  qed
  then show ?R using * by auto
qed

lemma mult2_ns_one_step:
  assumes "ns O s  s" "refl ns" "trans s"
  shows "(X, Y)  mult2_ns ns s  (X1 X2 Y1 Y2. X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw ns  (x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)))" (is "?L  ?R")
proof
  assume ?L then consider "(X, Y)  multpw ns" | "(X, Y)  mult2_s ns s"
    by (auto simp: mult2_s_def mult2_ns_def)
  then show ?R using mult2_s_one_step[OF assms]
    by (cases, intro exI[of _ "{#}", THEN exI[of _ Y, THEN exI[of _ "{#}", THEN exI[of _ X]]]]) auto
next
  assume ?R then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2"
    "(X1, Y1)  multpw ns" "x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)" by blast
  then show ?L using mult2_s_one_step[OF assms, of X Y] count_inject[of X2 "{#}"]
    by (cases "Y2 = {#}") (auto simp: mult2_s_def mult2_ns_def)
qed

lemma mult2_s_locally_one_step':
  assumes "ns O s  s" "refl ns" "locally_irrefl s X" "locally_irrefl s Y" "trans s"
  shows "(X, Y)  mult2_s ns s  (X1 X2 Y1 Y2. X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw ns  (X2, Y2)  mult s)" (is "?L  ?R")
proof
  assume ?L then show ?R unfolding mult2_s_one_step[OF assms(1,2,5)]
    using one_step_implies_mult[of _ _ s "{#}"] by auto metis
next
  assume ?R then obtain X1 X2 Y1 Y2 where x: "X = X1 + X2" and y: "Y = Y1 + Y2" and
    ns: "(X1, Y1)  multpw ns" and s: "(X2, Y2)  mult s" by blast
  then have l: "locally_irrefl s (X2 + Y1)" and r: "locally_irrefl s (Y2 + Y1)"
    using assms(3, 4) by (auto simp add: locally_irrefl_def)
  show ?L using ns s mult_locally_cancelL[OF assms(5) l r] multpw_add[OF ns, of X2 X2] refl_multpw[OF refl ns]
    unfolding mult2_s_def refl_on_def x y by auto
qed

lemma mult2_s_one_step':
  assumes "ns O s  s" "refl ns" "irrefl s" "trans s"
  shows "(X, Y)  mult2_s ns s  (X1 X2 Y1 Y2. X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw ns  (X2, Y2)  mult s)" (is "?L  ?R")
  using assms mult2_s_locally_one_step' by (simp add: mult2_s_locally_one_step' irrefl_def locally_irrefl_def) 

lemma mult2_ns_one_step':
  assumes "ns O s  s" "refl ns" "irrefl s" "trans s"
  shows "(X, Y)  mult2_ns ns s  (X1 X2 Y1 Y2. X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw ns  (X2, Y2)  (mult s)=)" (is "?L  ?R")
proof -
  have "(X, Y)  multpw ns  ?R"
    by (intro exI[of _ "{#}", THEN exI[of _ Y, THEN exI[of _ "{#}", THEN exI[of _ X]]]]) auto
  moreover have "X = X1 + Y2  Y = Y1 + Y2  (X1, Y1)  multpw ns  ?L" for X1 Y1 Y2
    using multpw_add[of X1 Y1 ns Y2 Y2] refl_multpw[OF refl ns] by (auto simp: mult2_ns_def refl_on_def)
  ultimately show ?thesis using mult2_s_one_step'[OF assms] unfolding mult2_ns_conv
    by auto blast
qed

subsection ‹Cancellation›

lemma mult2_s_locally_cancel1:
  assumes "s O ns  s" "ns O s  s" "refl ns" "trans ns" "locally_irrefl s (add_mset z X)" "locally_irrefl s (add_mset z Y)" "trans s"
    "(add_mset z X, add_mset z Y)  mult2_s ns s"
  shows "(X, Y)  mult2_s ns s"
proof -
  obtain X1 X2 Y1 Y2 where *: "add_mset z X = X1 + X2" "add_mset z Y = Y1 + Y2" "(X1, Y1)  multpw ns"
    "(X2, Y2)  mult s" using assms(8) unfolding mult2_s_locally_one_step'[OF assms(2,3,5,6,7)] by blast    
  from union_single_eq_member[OF this(1)] union_single_eq_member[OF this(2)] multi_member_split
  consider X1' where "X1 = add_mset z X1'" | Y1' where "Y1 = add_mset z Y1'"
    | X2' Y2' where "X2 = add_mset z X2'" "Y2 = add_mset z Y2'"
    unfolding set_mset_union Un_iff by metis
  then show ?thesis
  proof (cases)
    case 1 then obtain Y1' z' where **: "(X1', Y1')  multpw ns" "Y1 = add_mset z' Y1'" "(z, z')  ns"
      using * by (auto elim: multpw_split1R)
    then have "(X, Y1' + Y2)  mult2_s ns s" using * 1
      by auto (metis add_mset_add_single assms(2 - 7) li_trans_l mult2_s_locally_one_step') 
    moreover
    have "(Y1' + Y2, Y)  multpw ns"
      using refl_multpw[OF refl ns] * ** multpw_cancel1[OF trans ns **(3), of "Y1' + Y2" Y]
      by (auto simp: refl_on_def)
    ultimately show ?thesis using compat_mult2[OF assms(1,3,4)] unfolding mult2_ns_conv by blast
  next
    case 2 then obtain X1' z' where **: "(X1', Y1')  multpw ns" "X1 = add_mset z' X1'" "(z', z)  ns"
      using * by (auto elim: multpw_split1L)
    then have "(X1' + X2, Y)  mult2_s ns s" using * 2
      by auto (metis add_mset_add_single assms(2 - 7) li_trans_l mult2_s_locally_one_step')
    moreover
    have "(X, X1' + X2)  multpw ns"
      using refl_multpw[OF refl ns] * ** multpw_cancel1[OF trans ns **(3), of X "X1' + X2"]
      by (auto simp: refl_on_def)
    ultimately show ?thesis using compat_mult2[OF assms(1,3,4)] unfolding mult2_ns_conv by blast
  next
    case 3 then show ?thesis using assms *
      by (auto simp: mult2_s_locally_one_step' union_commute[of "{#_#}"] union_assoc[symmetric] mult_cancel mult_cancel_add_mset)
        (metis "*"(1) "*"(2) add_mset_add_single li_trans_l li_trans_r mult2_s_locally_one_step' mult_locally_cancel)
  qed
qed

lemma mult2_s_cancel1:
  assumes "s O ns  s" "ns O s  s" "refl ns" "trans ns" "irrefl s" "trans s" "(add_mset z X, add_mset z Y)  mult2_s ns s"
  shows "(X, Y)  mult2_s ns s"
  using assms mult2_s_locally_cancel1 by (metis irrefl_def locally_irrefl_def) 

lemma mult2_s_locally_cancel:
  assumes "s O ns  s" "ns O s  s" "refl ns" "trans ns" "locally_irrefl s (X + Z)" "locally_irrefl s (Y + Z)" "trans s"
  shows "(X + Z, Y + Z)  mult2_s ns s  (X, Y)  mult2_s ns s"
  using assms(5, 6)
proof (induct Z)
  case (add z Z) then show ?case
    using mult2_s_locally_cancel1[OF assms(1-4), of z "X + Z" "Y + Z"] 
    by auto (metis add_mset_add_single assms(7) li_trans_l) 
qed auto

lemma mult2_s_cancel:
  assumes "s O ns  s" "ns O s  s" "refl ns" "trans ns" "irrefl s" "trans s"
  shows "(X + Z, Y + Z)  mult2_s ns s  (X, Y)  mult2_s ns s"
  using mult2_s_locally_cancel assms by (metis irrefl_def locally_irrefl_def) 

lemma mult2_ns_cancel:
  assumes "s O ns  s" "ns O s  s" "refl ns" "trans s" "irrefl s" "trans ns"
  shows "(X + Z, Y + Z)  mult2_s ns s  (X, Y)  mult2_ns ns s"
  unfolding mult2_ns_conv using assms mult2_s_cancel multpw_cancel by blast

subsection ‹Implementation friendly versions of @{const mult2_s} and @{const mult2_ns}

definition mult2_alt :: "bool  'a rel  'a rel  'a multiset rel" where
  "mult2_alt b ns s = {(X, Y). (X1 X2 Y1 Y2. X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw ns  (b  Y2  {#})  (x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)))}"

lemma mult2_altI:
  assumes "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1)  multpw ns"
    "b  Y2  {#}" "x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)"
  shows "(X, Y)  mult2_alt b ns s"
  using assms unfolding mult2_alt_def by blast

lemma mult2_altE:
  assumes "(X, Y)  mult2_alt b ns s"
  obtains X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1)  multpw ns"
    "b  Y2  {#}" "x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)"
  using assms unfolding mult2_alt_def by blast

lemma mono_mult2_alt:
  assumes "ns  ns'" "s  s'" shows "mult2_alt b ns s  mult2_alt b ns' s'"
  unfolding mult2_alt_def using mono_multpw[OF assms(1)] assms by (blast 19)

abbreviation "mult2_alt_s  mult2_alt False"
abbreviation "mult2_alt_ns  mult2_alt True"

lemmas mult2_alt_s_def = mult2_alt_def[where b = False, unfolded simp_thms]
lemmas mult2_alt_ns_def = mult2_alt_def[where b = True, unfolded simp_thms]
lemmas mult2_alt_sI = mult2_altI[where b = False, unfolded simp_thms]
lemmas mult2_alt_nsI = mult2_altI[where b = True, unfolded simp_thms True_implies_equals]
lemmas mult2_alt_sE = mult2_altE[where b = False, unfolded simp_thms]
lemmas mult2_alt_nsE = mult2_altE[where b = True, unfolded simp_thms True_implies_equals]

paragraph ‹Equivalence to @{const mult2_s} and @{const mult2_ns}

lemma mult2_s_eq_mult2_s_alt:
  assumes "ns O s  s" "refl ns" "trans s"
  shows "mult2_alt_s ns s = mult2_s ns s"
  using mult2_s_one_step[OF assms] unfolding mult2_alt_s_def by blast

lemma mult2_ns_eq_mult2_ns_alt:
  assumes "ns O s  s" "refl ns" "trans s"
  shows "mult2_alt_ns ns s = mult2_ns ns s"
  using mult2_ns_one_step[OF assms] unfolding mult2_alt_ns_def by blast

lemma mult2_alt_local:
  assumes "(X, Y)  mult2_alt b ns s"
  shows "(X, Y)  mult2_alt b (ns  set_mset X × set_mset Y) (s  set_mset X × set_mset Y)"
proof -
  from assms obtain X1 X2 Y1 Y2 where *: "X = X1 + X2" "Y = Y1 + Y2" and
    "(X1, Y1)  multpw ns" "(b  Y2  {#})" "(x. x ∈# X2  (y. y ∈# Y2  (x, y)  s))"
    unfolding mult2_alt_def by blast
  then have "X = X1 + X2  Y = Y1 + Y2 
    (X1, Y1)  multpw (ns  set_mset X × set_mset Y)  (b  Y2  {#}) 
    (x. x ∈# X2  (y. y ∈# Y2  (x, y)  s  set_mset X × set_mset Y))"
    using multpw_local[of X1 Y1 ns]
      mono_multpw[of "ns  set_mset X1 × set_mset Y1" "ns  set_mset X × set_mset Y"] assms
    unfolding * set_mset_union unfolding set_mset_def by blast
  then show ?thesis unfolding mult2_alt_def by blast
qed

subsection ‹Local well-foundedness: restriction to downward closure of a set›

definition wf_below :: "'a rel  'a set  bool" where
  "wf_below r A = wf (Restr r ((r*)¯ `` A))"

lemma wf_below_UNIV[simp]:
  shows "wf_below r UNIV  wf r"
  by (auto simp: wf_below_def rtrancl_converse[symmetric] Image_closed_trancl[OF subset_UNIV])

lemma wf_below_mono1:
  assumes "r  r'" "wf_below r' A" shows "wf_below r A"
  using assms unfolding wf_below_def
  by (intro wf_subset[OF assms(2)[unfolded wf_below_def]] Int_mono Sigma_mono Image_mono
      iffD2[OF converse_mono] rtrancl_mono subset_refl)

lemma wf_below_mono2:
  assumes "A  A'" "wf_below r A'" shows "wf_below r A"
  using assms unfolding wf_below_def
  by (intro wf_subset[OF assms(2)[unfolded wf_below_def]]) blast

lemma wf_below_pointwise:
  "wf_below r A  (a. a  A  wf_below r {a})" (is "?L  ?R")
proof
  assume ?L then show ?R using wf_below_mono2[of "{_}" A r] by blast
next
  have *: "(r*)¯ `` A = {(r*)¯ `` {a} |a. a  A}" unfolding Image_def by blast
  assume ?R
  { fix x X assume *: "X  Restr r ((r*)¯ `` A) `` X" "x  X"
    then obtain a where **: "a  A" "(x, a)  r*" unfolding Image_def by blast
    from * have "X  ((r*)¯ `` {a})  (Restr r ((r*)¯ `` A) `` X)  ((r*)¯ `` {a})" by auto
    also have "...  Restr r ((r*)¯ `` {a}) `` (X   ((r*)¯ `` {a}))" unfolding Image_def by fastforce
    finally have "X  ((r*)¯ `` {a}) = {}" using ?R **(1) unfolding wf_below_def
      by (intro wfE_pf[of "Restr r ((r*)¯ `` {a})"]) (auto simp: Image_def)
    then have False using *(2) ** unfolding Image_def by blast
  }
  then show ?L unfolding wf_below_def by (intro wfI_pf) auto
qed

lemma SN_on_Image_rtrancl_conv:
  "SN_on r A  SN_on r (r* `` A)" (is "?L  ?R")
proof
  assume ?L then show ?R by (auto simp: SN_on_Image_rtrancl)
next
  assume ?R then show ?L by (auto simp: SN_on_def)
qed

lemma SN_on_iff_wf_below:
  "SN_on r A  wf_below (r¯) A"
proof -
  { fix f
    assume "f 0  r* `` A" and **: "(f i, f (Suc i))  r" for i
    then have "f i  r* `` A" for i
      by (induct i) (auto simp: Image_def, metis UnCI relcomp.relcompI rtrancl_unfold)
    then have "(f i, f (Suc i))  Restr r (r* `` A)" for i using ** by auto
  }
  moreover then have "SN_on r (r* `` A)  SN_on (Restr r (r* `` A)) (r* `` A)"
    unfolding SN_on_def by auto blast
  moreover have "(i. (f i, f (Suc i))  Restr r (r* `` A))  f 0  r* `` A" for f by auto
  then have "SN_on (Restr r (r* `` A)) (r* `` A)  SN_on (Restr r (r* `` A)) UNIV"
    unfolding SN_on_def by auto
  ultimately show ?thesis  unfolding SN_on_Image_rtrancl_conv [of _ A]
    by (simp add: wf_below_def SN_iff_wf rtrancl_converse converse_Int converse_Times)
qed


lemma restr_trancl_under:
  shows "Restr (r+) ((r*)¯ `` A) = (Restr r ((r*)¯ `` A))+"
proof (intro equalityI subrelI, elim IntE conjE[OF iffD1[OF mem_Sigma_iff]])
  fix a b assume *: "(a, b)  r+" "b  (r*)¯ `` A"
  then have "(a, b)  (Restr r ((r*)¯ `` A))+  a  (r*)¯ `` A"
  proof (induct rule: trancl_trans_induct[consumes 1])
    case 1 then show ?case by (auto simp: Image_def intro: converse_rtrancl_into_rtrancl)
  next
    case 2 then show ?case by (auto simp del: Int_iff del: ImageE)
  qed
  then show "(a, b)  (Restr r ((r*)¯ `` A))+" by simp
next
  fix a b assume "(a, b)  (Restr r ((r*)¯ `` A))+"
  then show "(a, b) : Restr (r+) ((r*)¯ `` A)" by induct auto
qed

lemma wf_below_trancl:
  shows "wf_below (r+) A  wf_below r A"
  using restr_trancl_under[of r A] by (simp add: wf_below_def wf_trancl_conv)

lemma wf_below_mult_local:
  assumes "wf_below r (set_mset X)" shows "wf_below (mult r) {X}"
    (* this is actually an equivalence; is the other direction useful as well? *)
proof -
  have foo: "mult r  mult (r+)" using mono_mult[of r "r+"] by force
  have "(Y, X)  (mult (r+))*  set_mset Y  ((r+)*)¯ `` set_mset X" for Y
  proof (induct rule: converse_rtrancl_induct)
    case (step Z Y)
    obtain I J K where *: "Y = I + J" "Z = I + K" "(k  set_mset K. j  set_mset J. (k, j)  r+)"
      using mult_implies_one_step[OF _ step(1)] by auto
    { fix k assume "k ∈# K"
      then obtain j where "j ∈# J" "(k, j)  r+" using *(3) by auto
      moreover then obtain x where "x ∈# X" "(j, x)  r*" using step(3) by (auto simp: *)
      ultimately have "x. x ∈# X  (k, x)  r*" by auto
    }
    then show ?case using * step(3) by (auto simp: Image_def) metis
  qed auto
  then have q: "(Y, X)  (mult (r+))*  y ∈# Y   y  ((r+)*)¯ `` set_mset X" for Y y by force
  have "Restr (mult (r+)) (((mult (r+))*)¯ `` {X})  mult (Restr (r+) (((r+)*)¯ `` set_mset X))"
  proof (intro subrelI)
    fix N M assume "(N, M)  Restr (mult (r+)) (((mult (r+))*)¯ `` {X})"
    then have **:  "(N, X)  (mult (r+))*" "(M, X)  (mult (r+))*" "(N, M)  mult (r+)" by auto
    obtain I J K where *: "M = I + J" "N = I + K" "J  {#}" "k  set_mset K. j  set_mset J. (k, j)  r+"
      using mult_implies_one_step[OF _ (N, M)  mult (r+)] by auto
    then show "(N, M)  mult (Restr (r+) (((r+)*)¯ `` set_mset X))"
      using q[OF **(1)] q[OF **(2)] unfolding * by (auto intro: one_step_implies_mult)
  qed
  note bar = subset_trans[OF Int_mono[OF foo Sigma_mono] this]
  have "((mult r)*)¯ `` {X}  ((mult (r+))*)¯ `` {X}" using foo by (simp add: Image_mono rtrancl_mono)
  then have "Restr (mult r) (((mult r)*)¯ `` {X})  mult (Restr (r+) (((r+)*)¯ `` set_mset X))"
    by (intro bar) auto
  then show ?thesis using wf_mult assms wf_subset
    unfolding wf_below_trancl[of r, symmetric] unfolding wf_below_def by blast
qed

lemma qc_wf_below:
  assumes "s O ns  (s  ns)* O s" "wf_below s A"
  shows "wf_below (ns* O s O ns*) A"
  unfolding wf_below_def
proof (intro wfI_pf)
  let ?A' = "((ns* O s O ns*)*)¯ `` A"
  fix X assume X: "X  Restr (ns* O s O ns*) ?A' `` X"
  let ?X' = "((s  ns)*  UNIV × ((s*)¯ `` A)) `` X"
  have *: "s O (s  ns)*  (s  ns)* O s"
  proof - (* taken from the proof of qc_wf_relto_iff *)
    { fix x y z assume "(y, z)  (s  ns)*" and "(x, y)  s"
      then have "(x, z)  (s  ns)* O s"
      proof (induct y z)
        case rtrancl_refl then show ?case by auto
      next
        case (rtrancl_into_rtrancl a b c)
        then have "(x, c)  ((s  ns)* O (s  ns)*) O s" using assms by blast
        then show ?case by simp
      qed }
    then show ?thesis by auto
  qed
  { fix x assume "x  Restr (ns* O s O ns*) ?A' `` X"
    then obtain y z where **: "y  X" "z  A" "(y, x)  ns* O s O ns*" "(x, z)  (ns* O s O ns*)*" by blast
    have "(ns* O s O ns*) O (ns* O s O ns*)*  (s  ns)*" by regexp 
    then have "(y, z)  (s  ns)*" using **(3,4) by blast
    moreover have "?X' = {}"
    proof (intro wfE_pf[OF assms(2)[unfolded wf_below_def]] subsetI)
      fix x assume "x  ?X'"
      then have "x  ((s  ns)*  UNIV × ((s*)¯ `` A)) `` Restr (ns* O s O ns*) ?A' `` X" using X by auto
      then obtain x0 y z where **: "z  X" "x0  A" "(z, y)  ns* O s O ns*" "(y, x)  (s  ns)*" "(x, x0)  s*"
        unfolding Image_def by blast
      have "(ns* O s O ns*) O (s  ns)*  ns* O (s O (s  ns)*)" by regexp
      with **(3,4) have "(z, x)  ns* O (s O (s  ns)*)" by blast
      moreover have "ns* O ((s  ns)* O s)  (s  ns)* O s" by regexp
      ultimately have "(z, x)  (s  ns)* O s" using * by blast
      then obtain x' where "z  X" "(z, x')  (s  ns)*"  "(x', x)  s" "(x', x0)  s*" "(x, x0)  s*" "x0  A"
        using **(1,2,5) converse_rtrancl_into_rtrancl[OF _ **(5)] by blast
      then show "x  Restr s ((s*)¯ `` A) `` ?X'"
        unfolding Image_def by blast
    qed
    ultimately have False using **(1,2) unfolding Image_def by blast 
  }
  then show "X = {}" using X by blast
qed

lemma wf_below_mult2_s_local:
  assumes "wf_below s (set_mset X)" "s O ns  s" "refl ns" "trans ns"
  shows "wf_below (mult2_s ns s) {X}"
  using wf_below_mult_local[of s X] assms multpw_mult_commute[of s ns]
    wf_below_mono1[of "multpw ns O mult s" "(multpw ns)* O mult s O (multpw ns)*" "{X}"]
    qc_wf_below[of "mult s" "multpw ns" "{X}"]
  unfolding mult2_s_def by blast


subsection ‹Trivial cases›

lemma mult2_alt_emptyL:
  "({#}, Y)  mult2_alt b ns s  b  Y  {#}"
  unfolding mult2_alt_def by auto

lemma mult2_alt_emptyR:
  "(X, {#})  mult2_alt b ns s  b  X = {#}"
  unfolding mult2_alt_def by (auto intro: multiset_eqI)

lemma mult2_alt_s_single:
  "(a, b)  s  ({#a#}, {#b#})  mult2_alt_s ns s"
  using mult2_altI[of _ "{#}" _ _ "{#}" _ ns False s] by auto

lemma multpw_implies_mult2_alt_ns:
  assumes "(X, Y)  multpw ns"
  shows "(X, Y)  mult2_alt_ns ns s"
  using assms by (intro mult2_alt_nsI[of X X "{#}" Y Y "{#}"]) auto

lemma mult2_alt_ns_conv:
  "mult2_alt_ns ns s = mult2_alt_s ns s  multpw ns" (is "?l = ?r")
proof (intro equalityI subrelI)
  fix X Y assume "(X, Y)  ?l"
  thm mult2_alt_nsE
  then obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1)  multpw ns"
    "x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)" by (auto elim: mult2_alt_nsE)
  then show "(X, Y)  ?r" using count_inject[of X2 "{#}"]
    by (cases "Y2 = {#}") (auto intro: mult2_alt_sI elim: mult2_alt_nsE mult2_alt_sE)
next
  fix X Y assume "(X, Y)  ?r" then show "(X, Y)  ?l"
    by (auto intro: mult2_alt_nsI multpw_implies_mult2_alt_ns elim: mult2_alt_sE)
qed

lemma mult2_alt_s_implies_mult2_alt_ns:
  assumes "(X, Y)  mult2_alt_s ns s"
  shows "(X, Y)  mult2_alt_ns ns s"
  using assms by (auto intro: mult2_alt_nsI elim: mult2_alt_sE)

lemma mult2_alt_add:
  assumes "(X1, Y1)  mult2_alt b1 ns s" and "(X2, Y2)  mult2_alt b2 ns s"
  shows "(X1 + X2, Y1 + Y2)  mult2_alt (b1  b2) ns s"
proof -
  from assms obtain X11 X12 Y11 Y12 X21 X22 Y21 Y22 where
    "X1 = X11 + X12" "Y1 = Y11 + Y12"
    "(X11, Y11)  multpw ns" "(b1  Y12  {#})" "(x. x ∈# X12  (y. y ∈# Y12  (x, y)  s))"
    "X2 = X21 + X22" "Y2 = Y21 + Y22"
    "(X21, Y21)  multpw ns" "(b2  Y22  {#})" "(x. x ∈# X22  (y. y ∈# Y22  (x, y)  s))"
    unfolding mult2_alt_def by (blast 9)
  then show ?thesis
    by (intro mult2_altI[of _ "X11 + X21" "X12 + X22" _ "Y11 + Y21" "Y12 + Y22"])
      (auto intro: multpw_add simp: ac_simps)
qed

lemmas mult2_alt_s_s_add = mult2_alt_add[of _ _ False _ _ _ _ False, unfolded simp_thms]
lemmas mult2_alt_ns_s_add = mult2_alt_add[of _ _ True _ _ _ _ False, unfolded simp_thms]
lemmas mult2_alt_s_ns_add = mult2_alt_add[of _ _ False _ _ _ _ True, unfolded simp_thms]
lemmas mult2_alt_ns_ns_add = mult2_alt_add[of _ _ True _ _ _ _ True, unfolded simp_thms]


lemma multpw_map:
  assumes "x y. x ∈# X  y ∈# Y  (x, y)  ns  (f x, g y)  ns'"
    and "(X, Y)  multpw ns"
  shows "(image_mset f X, image_mset g Y)  multpw ns'"
  using assms(2,1) by (induct X Y rule: multpw.induct) (auto intro: multpw.intros)

lemma mult2_alt_map:
  assumes "x y. x ∈# X  y ∈# Y  (x, y)  ns  (f x, g y)  ns'"
    and "x y. x ∈# X  y ∈# Y  (x, y)  s  (f x, g y)  s'"
    and "(X, Y)  mult2_alt b ns s"
  shows "(image_mset f X, image_mset g Y)  mult2_alt b ns' s'"
proof -
  from assms(3) obtain X1 X2 Y1 Y2 where "X = X1 + X2" "Y = Y1 + Y2" "(X1, Y1)  multpw ns"
    "b  Y2  {#}" "x. x ∈# X2  (y. y ∈# Y2  (x, y)  s)" by (auto elim: mult2_altE)
  moreover from this(1,2,5) have "x. x ∈# image_mset f X2  (y. y ∈# image_mset g Y2  (x, y)  s')"
    using assms(2) by (simp add: in_image_mset image_iff) blast
  ultimately show ?thesis using assms multpw_map[of X1 Y1 ns f g]
    by (intro mult2_altI[of _ "image_mset f X1" "image_mset f X2" _ "image_mset g Y1" "image_mset g Y2"]) auto
qed

text ‹Local transitivity of @{const mult2_alt}

lemma trans_mult2_alt_local:
  assumes ss: "x y z. x ∈# X  y ∈# Y  z ∈# Z  (x, y)  s  (y, z)  s  (x, z)  s"
    and ns: "x y z. x ∈# X  y ∈# Y  z ∈# Z  (x, y)  ns  (y, z)  s  (x, z)  s"
    and sn: "x y z. x ∈# X  y ∈# Y  z ∈# Z  (x, y)  s  (y, z)  ns  (x, z)  s"
    and nn: "x y z. x ∈# X  y ∈# Y  z ∈# Z  (x, y)  ns  (y, z)  ns  (x, z)  ns"
    and xyz: "(X, Y)  mult2_alt b1 ns s" "(Y, Z)  mult2_alt b2 ns s"
  shows "(X, Z)  mult2_alt (b1  b2) ns s"
proof -
  let ?a1 = Enum.finite_3.a1 and ?a2 = Enum.finite_3.a2 and ?a3 = Enum.finite_3.a3
  let ?t = "{(?a1, ?a2), (?a1, ?a3), (?a2, ?a3)}"
  let ?A = "{(?a1, x) |x. x ∈# X}  {(?a2, y) |y. y ∈# Y}  {(?a3, z) |z. z ∈# Z}"
  define s' where "s' = Restr {((a, x), (b, y)) |a x b y. (a, b)  ?t  (x, y)  s} ?A"
  define ns' where "ns' = (Restr {((a, x), (b, y)) |a x b y. (a, b)  ?t  (x, y)  ns} ?A)="
  have *: "refl ns'" "trans ns'" "trans s'" "s' O ns'  s'" "ns' O s'  s'"
    by (force simp: trans_def ss ns sn nn s'_def ns'_def)+
  have "({#(?a1, x). x ∈# X#}, {#(?a2, y). y ∈# Y#})  mult2_alt b1 ns' s'"
    by (auto intro: mult2_alt_map[OF _ _ xyz(1)] simp: s'_def ns'_def)
  moreover have "({#(?a2, y). y ∈# Y#}, {#(?a3, z). z ∈# Z#})  mult2_alt b2 ns' s'"
    by (auto intro: mult2_alt_map[OF _ _ xyz(2)] simp: s'_def ns'_def)
  ultimately have "({#(?a1, x). x ∈# X#}, {#(?a3, z). z ∈# Z#})  mult2_alt (b1  b2) ns' s'"
    using mult2_s_eq_mult2_s_alt[OF *(5,1,3)] mult2_ns_eq_mult2_ns_alt[OF *(5,1,3)]
      trans_mult2_s[OF *(4,1,2)] trans_mult2_ns[OF *(4,1,2)] compat_mult2[OF *(4,1,2)]
    by (cases b1; cases b2) (auto simp: trans_O_iff)
  from mult2_alt_map[OF _ _ this, of snd snd ns s]
  show ?thesis by (auto simp: s'_def ns'_def image_mset.compositionality comp_def in_image_mset image_iff)
qed

lemmas trans_mult2_alt_s_s_local = trans_mult2_alt_local[of _ _ _ _ _ False False, unfolded simp_thms]
lemmas trans_mult2_alt_ns_s_local = trans_mult2_alt_local[of _ _ _ _ _ True False, unfolded simp_thms]
lemmas trans_mult2_alt_s_ns_local = trans_mult2_alt_local[of _ _ _ _ _ False True, unfolded simp_thms]
lemmas trans_mult2_alt_ns_ns_local = trans_mult2_alt_local[of _ _ _ _ _ True True, unfolded simp_thms]

end