Theory FCF_Multiset

theory FCF_Multiset
  imports 
    FCF_Set
    Pattern_Completeness_Multiset
begin

fun depth_gterm :: "('f,'v)term ⇒ nat" where
  "depth_gterm (Fun f ts) = Suc (max_list (map depth_gterm ts))" 
| "depth_gterm _ = Suc 0" 

lemma depth_gterm_arg: "t ∈ set ts ⟹ depth_gterm t < depth_gterm (Fun f ts)" 
  unfolding less_eq_Suc_le by (auto intro: max_list)


(* **************************************** 
     MULTISET LEVEL 
   *****************************************)

type_synonym('f,'s)simple_match_problem_ms = "('f,nat × 's)term multiset multiset"

type_synonym('f,'s)simple_pat_problem_ms = "('f,'s)simple_match_problem_ms multiset"

abbreviation mset2 :: "('f,'s)simple_match_problem_ms ⇒ ('f,'s)simple_match_problem" where
  "mset2 ≡ image set_mset o set_mset" 

abbreviation mset3 :: "('f,'s)simple_pat_problem_ms ⇒ ('f,'s)simple_pat_problem" where
  "mset3 ≡ image mset2 o set_mset" 

lemma mset2_simps: 
  "mset2 (add_mset eq mp) = insert (set_mset eq) (mset2 mp)"
  "set_mset (add_mset t eq) = insert t (set_mset eq)" 
  "set_mset {#} = {}" 
  "mset2 (mp1 + mp2) = mset2 mp1 ∪ mset2 mp2" 
  "mset3 (add_mset mp p) = insert (mset2 mp) (mset3 p)"
  by auto

context pattern_completeness_context
begin
 
inductive smp_step_ms :: "('f,'s)simple_match_problem_ms ⇒ ('f,'s)simple_match_problem_ms ⇒ bool"
  (infix ‹→⇩s⇩s› 50) where
  smp_dup: "add_mset (add_mset t (add_mset t eqc)) mp →⇩s⇩s add_mset (add_mset t eqc) mp" 
| smp_singleton: "add_mset {# t #} mp →⇩s⇩s mp" 
| smp_triv_sort: "t : ι in 𝒯(C,𝒱) ⟹ cd_sort ι = 1 ⟹ add_mset (add_mset t eq) mp →⇩s⇩s mp" 
| smp_decomp: "(⋀ t. t ∈ set_mset eqc ⟹ root t = Some (f,n))
    ⟹ eqcn = {#{#args t ! i. t ∈# eqc#}. i ∈# mset [0..<n]#}
    ⟹ (⋀ eq. eq ∈ set_mset eqcn ⟹ UNIQ (𝒯(C,𝒱) ` set_mset eq))
    ⟹ add_mset eqc mp →⇩s⇩s eqcn + mp"  

inductive smp_fail_ms :: "('f,'s)simple_match_problem_ms ⇒ bool" where
  smp_clash: "Conflict_Clash s t ⟹ 
      s ∈ eqc ⟹ t ∈ eqc ⟹ eqc ∈ mset2 mp ⟹ smp_fail_ms mp" 
| smp_decomp_fail: "(⋀ t. t ∈ set_mset eqc ⟹ root t = Some (f,n))
    ⟹ i < n 
    ⟹ ¬ UNIQ (𝒯(C,𝒱) ` (λ t. args t ! i) ` set_mset eqc)
    ⟹ smp_fail_ms (add_mset eqc mp)" 
 
inductive spp_step_ms :: "('f,'s)simple_pat_problem_ms ⇒ ('f,'s)simple_pat_problem_ms multiset ⇒ bool"
  (infix ‹⇒⇩s⇩s› 50) where
  spp_solved: "add_mset {#} p ⇒⇩s⇩s {#}" 
| spp_simp: "mp →⇩s⇩s mp' ⟹ add_mset mp p ⇒⇩s⇩s {#add_mset mp' p#}" 
| spp_delete: "smp_fail_ms mp ⟹ add_mset mp p ⇒⇩s⇩s {#p#}"
| spp_delete_large_sort: "
    (⋀ i. i ≤ (n :: nat) ⟹ snd (x i) = ι ∧ eq i ∈# mp i ∧ Var (x i) ≠ t i ∧ {Var (x i), t i} ⊆ set_mset (eq i)) ⟹
    x ` {0..n} ∩ tvars_spat (mset3 p) = {} ⟹
    (card (t ` {0..n}) < card_of_sort C ι) ⟹
    p + mset (map mp [0..< Suc n]) ⇒⇩s⇩s {# p #}" 
| spp_inst: "{#{#Var x, t#}#} ∈# p 
   ⟹ is_Fun t 
   ⟹ fst ` tvars_spat (mset3 p) ∩ {n..<n + m} = {}
   ⟹ p ⇒⇩s⇩s mset (map (λ τ. image_mset (image_mset (image_mset (λt. t ⋅ τ))) p) (τs_list n x))" 
| spp_split: "mp = add_mset (add_mset s (add_mset t eqc)) mp'
   ⟹ is_Var s ≠ is_Var t ⟹ eqc ≠ {#} ∨ mp' ≠ {#}
   ⟹ add_mset mp p ⇒⇩s⇩s {#add_mset {# {# s, t #} #} p, add_mset (add_mset (add_mset s eqc) mp') p#}" 
end

context pattern_completeness_context_with_assms
begin

lemma smp_fail_ms: assumes "smp_fail_ms mp"
  and "finite_constructor_form_pat (insert (mset2 mp) p)" 
shows "finite_constructor_form_pat p" 
  "simple_pat_complete C SS (insert (mset2 mp) p) ⟷ simple_pat_complete C SS p"
proof -
  show "finite_constructor_form_pat p" using assms(2) unfolding finite_constructor_form_pat_def by auto
  show "simple_pat_complete C SS (insert (mset2 mp) p) ⟷ simple_pat_complete C SS p"
    using assms
  proof (induct mp rule: smp_fail_ms.induct)
    case *: (smp_clash s t eqc mp)
    from *(4) obtain eq mp' where mp: "mp = add_mset eq mp'" and eqc: "eqc = set_mset eq"
      by (metis comp_apply image_iff mset_add)
    from eqc *(2-3) have "set_mset eq = {s,t} ∪ eqc" by auto
    from eliminate_clash_spp(1)[OF *(5)[unfolded mset2_simps mp] refl refl this *(1)]
    show ?case unfolding mp mset2_simps .
  next
    case *: (smp_decomp_fail eqc f n i mp)
    from *(2-3) have "(∀eq∈{{args t ! i |. t ∈ set_mset eqc} |. i ∈ {0..<n}}. UNIQ (𝒯(C,𝒱) ` eq)) = False" 
      by auto
    from decompose_spp(1)[OF *(4)[unfolded mset2_simps] refl refl *(1) refl refl, unfolded this if_False]
    show ?case unfolding mset2_simps by auto
  qed
qed
  

lemma smp_step_ms: assumes "mp →⇩s⇩s mp'"
  and "finite_constructor_form_pat (insert (mset2 mp) p)" 
shows "finite_constructor_form_pat (insert (mset2 mp') p)" 
  "simple_pat_complete C SS (insert (mset2 mp) p) ⟷ simple_pat_complete C SS (insert (mset2 mp') p)" 
proof (atomize(full), insert assms, induct mp mp' rule: smp_step_ms.induct)
  case (smp_singleton t mp)
  from eliminate_uniq_spp[OF this[unfolded mset2_simps] refl refl refl]
  show ?case by (auto simp: Uniq_def)
next
  case *: (smp_triv_sort t ι eq mp)
  show ?case 
  proof (intro conjI)
    show "finite_constructor_form_pat (insert (mset2 mp) p)" 
      using * unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def by auto
    show "simple_pat_complete C SS (insert (mset2 (add_mset (add_mset t eq) mp)) p) =
      simple_pat_complete C SS (insert (mset2 mp) p)" 
      unfolding simple_pat_complete_def bex_simps
    proof (rule all_cong, intro disj_cong refl)
      fix σ
      assume sig: "σ :⇩s 𝒱 |` SS → 𝒯(C)" 
      from * obtain τ where typed: "u ∈ insert t (set_mset eq) ⟹ u : τ in 𝒯(C,𝒱 |` SS)" for u 
        unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def by auto
      from typed_S_eq[OF this *(1)] have tau: "τ = ι" by auto
      from typed_imp_S[OF typed, of t] tau have "ι ∈ S" by auto
      from cd[OF this] * k1
      have card: "card_of_sort C ι = 1" by auto
      have "UNIQ_subst σ (insert t (set_mset eq))" unfolding UNIQ_subst_alt_def
      proof (intro allI impI, goal_cases)
        case (1 u v)
        {
          fix w
          assume "w ∈ {u,v}" 
          with 1 typed tau have "w : ι in 𝒯(C,𝒱 |` SS)" by auto
          with sig have "w ⋅ σ : ι in 𝒯(C)" by (rule subst_hastype)
        }
        hence "u ⋅ σ : ι in 𝒯(C)" "v ⋅ σ : ι in 𝒯(C)" by auto
        with card
        show "u ⋅ σ = v ⋅ σ" unfolding card_of_sort_def card_eq_1_iff by auto
      qed
      thus "simple_match_complete_wrt σ (mset2 (add_mset (add_mset t eq) mp)) =
         simple_match_complete_wrt σ (mset2 mp)" 
        unfolding simple_match_complete_wrt_def by simp
    qed
  qed
next
  case *: (smp_decomp eqc f n eqcn mp)
  have eq: "(∀eq∈mset2 eqcn. UNIQ (𝒯(C,𝒱) ` eq)) = True" 
    using *(2-3) by auto
  define N where "N = {0..<n}" 
  have fin: "finite N" unfolding N_def by auto
  have "mset2 eqcn = {{args t ! i |. t ∈ set_mset eqc} |. i ∈ {0..<n}}" 
    unfolding *(2) mset_upt N_def[symmetric] 
    apply (subst (2) finite_set_mset_mset_set[OF fin, symmetric])
    by (metis (no_types, lifting) comp_apply image_cong image_image multiset.set_map)
  from decompose_spp[OF *(4)[unfolded mset2_simps] refl refl *(1) this, unfolded eq if_True, OF _ refl]
  show ?case unfolding mset2_simps by auto
qed auto

lemma spp_step_ms_size: assumes "p ⇒⇩s⇩s Q" and "q ∈# Q" 
  shows "size q ≤ size p" 
  using assms by (cases, auto)
  

lemma spp_step_ms: assumes "p ⇒⇩s⇩s Pn"
  and "finite_constructor_form_pat (mset3 p)" 
shows "Ball (set_mset Pn) (λ p'. finite_constructor_form_pat (mset3 p'))" 
  "simple_pat_complete C SS (mset3 p) ⟷ Ball (set_mset Pn) (λ p'. simple_pat_complete C SS (mset3 p'))"
proof (atomize(full), insert assms, induct p Pn rule: spp_step_ms.induct)
  case (spp_solved p)  
  show ?case unfolding mset2_simps using detect_sat_spp by auto
next
  case *: (spp_simp mp mp' p)
  from smp_step_ms[OF *(1) *(2)[unfolded mset2_simps]]
  show ?case unfolding mset2_simps by auto
next
  case *: (spp_delete mp p)
  from smp_fail_ms[OF *(1) *(2)[unfolded mset2_simps]]
  show ?case unfolding mset2_simps by auto
next
  case *: (spp_inst x t p n)
  from mset_add[OF *(1)] have mem: "{{Var x,t}} ∈ mset3 p" by fastforce
  define p' where "p' = mset3 p" 
  have id: "{(`) ((`) (λt. t ⋅ τ)) ` mset3 p |. τ ∈ τs n x} = mset3 ` {image_mset (image_mset (image_mset (λt. t ⋅ τ))) p |. τ ∈ τs n x}" 
    unfolding image_comp o_def image_mset.comp set_image_mset by auto
  from mem have "x ∈ tvars_spat (mset3 p)" unfolding p'_def[symmetric] 
    by (auto intro!: bexI[of _ "{{Var x, t}}"])
  from instantiate_spp[OF *(4,3) this refl]
  show ?case unfolding id using τs_list by auto
next
  case *: (spp_split mp s t eqc mp' p)
  have "insert s (insert t (set_mset eqc)) = {s, t} ∪ set_mset eqc" by auto
  from separate_var_fun_spp_single[OF *(4)[unfolded mset2_simps *(1)] refl refl this refl]
  show ?case unfolding mset2_simps *(1) by auto
next
  case *: (spp_delete_large_sort n x ι eq mp t p)
  have "mset3 (p + mset (map mp [0..<Suc n])) = mset3 p ∪ (mset2 o mp) ` set [0..< Suc n]" 
    by auto
  also have "set [0..< Suc n] = {0..n}" by auto
  finally have id: "mset3 (p + mset (map mp [0..<Suc n])) = mset3 p ∪ (mset2 ∘ mp) ` {0..n} " by auto
  have main: "simple_pat_complete C SS (mset3 (p + mset (map mp [0..<Suc n]))) = 
     simple_pat_complete C SS (mset3 p)" unfolding id
    apply (rule eliminate_large_sort[OF _ *(2,3), of "set_mset o eq"])
    subgoal for i using *(1)[of i] by auto
    subgoal using *(4) unfolding id by (auto simp: finite_constructor_form_pat_def)
    done
  show ?case unfolding main using *(4) by (auto simp: finite_constructor_form_pat_def)
qed

lemma finite_tvars_spat_mset3: "finite (tvars_spat (mset3 p))" 
  by (intro finite_Union; fastforce)  

lemma finite_tvars_smp_mset2: "finite (tvars_smp (mset2 mp))" 
  by (intro finite_Union; fastforce)  

lemma normal_form_spp_step_fvf: assumes "finite_constructor_form_pat (mset3 p)" 
  and "∄ P. p ⇒⇩s⇩s P ∧ P ≠ {#}" 
  and mp: "mp ∈ mset3 p" 
  and eqc: "eqc ∈ mp"
  and t: "t ∈ eqc" 
shows "is_Var t" 
proof (rule ccontr)
  assume f: "is_Fun t"  
  from mp obtain mp' where mp': "mp' ∈ set_mset p" and mp: "mp = mset2 mp'" by auto
  from eqc[unfolded mp] obtain eqc' where eqc': "eqc' ∈ set_mset mp'" and eqc: "eqc = set_mset eqc'" by auto
  from t[unfolded eqc] obtain eqc2 where id1: "eqc' = add_mset t eqc2" by (rule mset_add)
  from eqc' obtain mp2 where id2: "mp' = add_mset eqc' mp2" by (rule mset_add)
  from mp' obtain p2 where id3: "p = add_mset mp' p2" by (rule mset_add)
  have p: "p = add_mset (add_mset (add_mset t eqc2) mp2) p2" unfolding id1 id2 id3 ..
  with assms have contra: "add_mset (add_mset (add_mset t eqc2) mp2) p2 ⇒⇩s⇩s P ⟹ P ≠ {#} ⟹ False" for P by auto
  from assms(1)[unfolded finite_constructor_form_pat_def p] 
  have fin: "finite_constructor_form_mp (mset2 (add_mset (add_mset t eqc2) mp2))" by auto
  show False
  proof (cases "eqc2 = {#}")
    case True
    show False  
      apply (rule contra)
      apply (unfold True)
      by (rule spp_simp, rule smp_singleton, auto)
  next
    case ne: False   
    show False
    proof (cases "∃ s ∈ set_mset eqc2. is_Var s")
      case True
      then obtain s eqc3 where "eqc2 = add_mset s eqc3" and "is_Var s" by (metis mset_add)
      then obtain x where eqc: "add_mset t eqc2 = add_mset (Var x) (add_mset t eqc3)" by (cases s, auto)
      from fin[unfolded eqc finite_constructor_form_mp_def] obtain ι 
        where "Var x : ι in 𝒯(C,𝒱 |` SS)" by auto
      hence xS: "snd x ∈ S" unfolding hastype_def by (auto simp: restrict_map_def split: if_splits)
      show False
      proof (cases "eqc3 = {#} ∧ mp2 = {#}")
        case True
        hence True: "eqc3 = {#}" "mp2 = {#}" by auto
        define names where "names = fst ` ⋃ (⋃ (⋃ ((`) ((`) vars) ` insert (insert {Var x, t} (mset2 {#})) (mset3 p2))))" 
        define n where "n = Max names" 
        have id: "mset3 (add_mset {#{#Var x, t#}#} p2) = 
             insert (insert {Var x, t} (mset2 {#})) (mset3 p2)" by auto
        have "names = fst ` tvars_spat (mset3 p)" unfolding p eqc True names_def by simp
        also have "finite …" using finite_tvars_spat_mset3[of p] by blast
        finally have names: "⋀ k. k ∈ names ⟹ k ≤ n" unfolding n_def by auto
        from not_empty_sort[OF xS, unfolded empty_sort_def]
        obtain t where "t : snd x in 𝒯(C)" by auto 
        then obtain f ss where "f : ss → snd x in C" 
          by (induct, auto)
        hence "set (Cl (snd x)) ≠ {}" unfolding Cl by auto
        hence Cl: "Cl (snd x) ≠ []" by auto
        show False 
          apply (rule contra)
          apply (unfold eqc, unfold True)
          apply (rule spp_inst[OF _ f, of x _ "Suc n"])
           apply force
          apply (unfold id)
           apply (unfold names_def[symmetric])
           apply (insert names, fastforce)
          apply (insert Cl, auto simp: τs_list_def)
          done
      next
        case False
        hence diff: "eqc3 ≠ {#} ∨ mp2 ≠ {#}" by auto
        from contra[OF spp_split[OF _ _ diff], unfolded eqc True, OF refl] f
        show ?thesis by auto
      qed
    next
      case False
      hence funs: "⋀ s. s ∈# eqc2 ⟹ is_Fun s" by auto
      show False
      proof (cases "∃ s ∈# eqc2. root s ≠ root t")
        case True
        then obtain s eqc3 where eqc2: "eqc2 = add_mset s eqc3" and diff: "root s ≠ root t" 
          by (meson mset_add)
        from funs[of s] eqc2 diff f obtain f g where rt: "root t = Some f" "root s = Some g" and diff: "f ≠ g" 
          by (cases s; cases t; auto)
        hence conf: "Conflict_Clash s t" by (cases s; cases t; auto simp: conflicts.simps)
        show False 
          apply (rule contra)
          apply (unfold eqc2)
          apply (rule spp_delete)
          apply (rule smp_clash[OF conf, of "insert t (insert s (set_mset eqc3))"])
          by auto
      next
        case False
        from f obtain f n where "root t = Some (f,n)" by (cases t, auto)
        with False have rt: "⋀ s. s ∈# add_mset t eqc2 ⟹ root s = Some (f,n)" by auto
        let ?cond = "∀ eq ∈# {#{#args t ! i. t ∈# add_mset t eqc2#}. i ∈# mset [0..<n]#}. UNIQ (𝒯(C,𝒱) ` set_mset eq)" 
        show False
        proof (cases ?cond)
          case True
          show False
            apply (rule contra)
            apply (rule spp_simp)
            apply (rule smp_decomp[OF rt refl])
            using True by auto
        next
          case False
          define eqc3 where "eqc3 = add_mset t eqc2" 
          from False obtain i where i: "i < n" and nuniq: "¬ UNIQ (𝒯(C,𝒱) ` set_mset {#args t ! i. t ∈# add_mset t eqc2 #})" 
            unfolding mset2_simps by auto
          show False
            apply (rule contra)
            apply (rule spp_delete)
            apply (rule smp_decomp_fail[OF rt i])
            using nuniq by auto
        qed
      qed
    qed
  qed
qed

text ‹Every normal form consists purely of variables, and these variable are of sorts
  that have a small cardinality (upper bound is the number of matching problems in p).›
lemma NF_spp_step_fvf_with_small_card: assumes "finite_constructor_form_pat (mset3 p)" 
  and "∄ P. p ⇒⇩s⇩s P ∧ P ≠ {#}" 
  and mp: "mp ∈# p" 
  and eqc: "eqc ∈# mp"
  and t: "t ∈# eqc" 
shows "∃ x ι. t = Var (x,ι) ∧ card_of_sort C ι ≤ size p"
proof -
  from normal_form_spp_step_fvf[OF assms(1-2), of "mset2 mp" "set_mset eqc" t] mp eqc t
  obtain x ι where tx: "t = Var (x,ι)" by force
  from assms(1)[unfolded finite_constructor_form_pat_def finite_constructor_form_mp_def, 
      rule_format, of "mset2 mp" "set_mset eqc"] mp eqc t tx 
  have ts: "t : ι in 𝒯(C,𝒱 |` SS)" 
    by auto (metis Term.simps(1) comp_eq_dest_lhs hastype_def snd_eqD typed_S_eq)
  with tx have iota: "ι ∈ S" by (metis typed_imp_S)  
  show ?thesis
  proof (intro exI conjI, rule tx)
    show "card_of_sort C ι ≤ size p" 
    proof (rule ccontr)
      assume "¬ ?thesis" 
      hence large: "card_of_sort C ι > size p" by auto
      define filt where "filt mp = (∃ eqc ∈# mp. ∃ t ∈# eqc. t : ι in 𝒯(C, 𝒱 |` SS))" for mp
      define p1 where "p1 = filter_mset filt p" 
      define p2 where "p2 = filter_mset (Not o filt) p" 
      have p: "p = p1 + p2" unfolding p1_def p2_def by auto
      have large: "card_of_sort C ι > size p1" using large unfolding p by auto
      have mp: "mp ∈# p1" unfolding p1_def filt_def using mp eqc t ts by auto
      hence p1: "p1 ≠ {#}" by auto
      obtain p1l where p1l: "p1 = mset p1l" by (metis ex_mset)
      have len: "length p1l = size p1" unfolding p1l by auto
      with p1 obtain n where lenp: "length p1l = Suc n" by (cases p1l, auto)
      define mp where "mp i = p1l ! i" for i
      {
        fix i
        assume "i ≤ n" 
        hence "i < length p1l" unfolding lenp by auto
        hence "mp i ∈ set p1l" unfolding mp_def by auto
        hence mp: "mp i ∈# p1" unfolding p1l by auto
        from this[unfolded p1_def] have mpp: "mp i ∈# p" and filt: "filt (mp i)" by auto
        from assms(1)[unfolded finite_constructor_form_pat_def] mpp
        have fin: "finite_constructor_form_mp (mset2 (mp i))" by auto
        from filt[unfolded filt_def] obtain eqc t where eqc: "eqc ∈# mp i" 
          and t: "t ∈# eqc" and ts: "t : ι in 𝒯(C,𝒱 |` SS)" 
          by auto
        from fin[unfolded finite_constructor_form_mp_def, rule_format, of "set_mset eqc"] eqc
        obtain ι' where eqcs: "⋀ s. s ∈#eqc ⟹ s : ι' in 𝒯(C,𝒱 |` SS)" by auto
        from eqcs[OF t] ts have "ι' = ι" by fastforce
        note eqcs = eqcs[unfolded this]
        {
          fix mp'
          assume "mp i →⇩s⇩s mp'"        
          from spp_simp[OF this, of "p - {# mp i #}"] mpp
          have "∃ P. p ⇒⇩s⇩s P ∧ P ≠ {#}" by auto
          with assms have False by auto
        } note nf = this
        from eqc obtain mp' where mpi: "mp i = add_mset eqc mp'" by (metis mset_add)
        from t obtain eqc' where eqct: "eqc = add_mset t eqc'" by (metis mset_add)
        from smp_singleton[of t mp'] nf[unfolded mpi eqct] have "eqc' ≠ {#}" by auto
        then obtain s eqc2 where "eqc' = add_mset s eqc2" by (cases eqc', auto)
        note eqct = eqct[unfolded this]
        from smp_dup[of t eqc2 mp'] nf[unfolded mpi eqct] 
        have st: "s ≠ t" by auto
        from eqct have s: "s ∈# eqc" by auto
        from normal_form_spp_step_fvf[OF assms(1-2), of "mset2 (mp i)" "set_mset eqc", OF _ _ this]
          mpp eqc obtain x where sx: "s = Var x" by auto
        from eqcs[OF s, unfolded sx] have snd: "snd x = ι"
          by (metis Term.simps(1) comp_apply hastypeD option.inject typed_restrict_imp_typed)
        have summary: 
          "snd x = ι ∧ eqc ∈# mp i ∧ Var x ≠ t ∧ {Var x, t} ⊆ set_mset eqc ∧ t : ι in 𝒯(C,𝒱 |` SS)" 
          using st snd eqc eqct sx ts by auto
        hence "∃ x eqc t. snd x = ι ∧ eqc ∈# mp i ∧ Var x ≠ t ∧ {Var x, t} ⊆ set_mset eqc ∧ t : ι in 𝒯(C,𝒱 |` SS)" by blast
      }
      hence "∀ i. ∃ x eqc t. i ≤ n ⟶ snd x = ι ∧ eqc ∈# mp i ∧ Var x ≠ t ∧ {Var x, t} ⊆ set_mset eqc ∧ t : ι in 𝒯(C,𝒱 |` SS)" by blast
      from choice[OF this] obtain x where 
        "∀ i. ∃ eqc t. i ≤ n ⟶ snd (x i) = ι ∧ eqc ∈# mp i ∧ Var (x i) ≠ t ∧ {Var (x i), t} ⊆ set_mset eqc ∧ t : ι in 𝒯(C,𝒱 |` SS)" by blast
      from choice[OF this] obtain eqc where 
        "∀ i. ∃ t. i ≤ n ⟶ snd (x i) = ι ∧ eqc i ∈# mp i ∧ Var (x i) ≠ t ∧ {Var (x i), t} ⊆ set_mset (eqc i) ∧ t : ι in 𝒯(C,𝒱 |` SS)" by blast
      from choice[OF this] obtain t where 
        witnesses: "⋀ i. i ≤ n ⟹ snd (x i) = ι ∧ eqc i ∈# mp i ∧ Var (x i) ≠ t i ∧ {Var (x i), t i} ⊆ set_mset (eqc i)"
          and ti: "⋀ i. i ≤ n ⟹ t i : ι in 𝒯(C,𝒱 |` SS)" by blast
      note step = spp_delete_large_sort[of n x ι eqc mp t p2, OF witnesses] 
      have "card (t ` {0..n}) ≤ card {0..n}" using card_image_le by blast
      also have "… = size p1" using len lenp p1l by auto
      also have "… < card_of_sort C ι" by fact
      finally have "card (t ` {0..n}) < card_of_sort C ι" . 
      note step = step[OF _ _ this]
      have id: "map mp [0..<Suc n] = p1l" unfolding mp_def using lenp by (rule map_nth')
      have "p2 + mset (map mp [0..<Suc n]) = p" unfolding id p p1l by auto
      note step = step[unfolded this]
      let ?Var = "Var :: nat × 's ⇒ ('f, nat × 's) Term.term" 
      define Vs where "Vs = tvars_spat (mset3 p2)" 
      have "x ` {0..n} ∩ tvars_spat (mset3 p2) = {}"
      proof (rule ccontr)
        assume "¬ ?thesis" 
        then obtain s where s1: "s ∈ x ` {0..n}" 
           and s2: "s ∈ tvars_spat (mset3 p2)" unfolding Vs_def[symmetric] by blast
        from s1 obtain i where "i ≤ n" and s: "s = x i" by auto
        with witnesses[of i] ti[of i] have sι: "Var s : ι in 𝒯(C,𝒱)"
          by (metis Term.simps(1) comp_eq_dest_lhs hastypeI)
        from s2 obtain mp eqc u where *: "mp ∈# p2" "eqc ∈# mp" "u ∈# eqc" "s ∈ vars u"  
          by fastforce
        from *(1)[unfolded p2_def] have mp: "mp ∈# p" and "¬ filt mp" by auto
        from this(2)[unfolded filt_def] * have ns: "¬ u : ι in 𝒯(C,𝒱 |` SS)" by auto
        from normal_form_spp_step_fvf[OF assms(1-2), of "mset2 mp" "set_mset eqc" u] mp *
        have "is_Var u" by auto
        with * have u: "u = Var s" by auto
        note ns = ns[unfolded this]
        from sι iota u ns show False
          by (smt (verit, del_insts) SigmaE SigmaI UNIV_I UNIV_Times_UNIV Var_hastype comp_apply eq_Some_iff_hastype
              hastype_restrict option.inject snd_conv)  
      qed
      note step = step[OF _ this]
      from step assms(2) show False by auto
    qed
  qed
qed


definition max_depth_sort :: "'s ⇒ nat" where
  "max_depth_sort s = Maximum (depth_gterm ` {t. t : s in 𝒯(C)})" 

lemma max_depth_sort_wit: assumes "finite_sort C s" 
  and "s ∈ S" 
shows "∃ t. t : s in 𝒯(C) ∧ 
    depth_gterm t = max_depth_sort s ∧ 
    (∀ t'. t' : s in 𝒯(C) ⟶ depth_gterm t' ≤ depth_gterm t)"
proof -
  let ?T = "{t. t : s in 𝒯(C)}" 
  from sorts_non_empty[OF assms(2)] have "depth_gterm ` ?T ≠ {}" by auto
  moreover from assms(1)[unfolded finite_sort_def] have fin: "finite (depth_gterm ` ?T)" by auto
  ultimately obtain d where "d ∈ depth_gterm ` ?T" and d: "d = Maximum (depth_gterm ` ?T)"
    by (metis has_MaximumD(1) has_Maximum_nat_iff_finite)
  from this obtain t where t: "t ∈ ?T" 
    and depth: "depth_gterm t = Maximum (depth_gterm ` ?T)" "d = depth_gterm t" by auto
  have "t' ∈ ?T ⟹ depth_gterm t' ≤ depth_gterm t" for t' 
    unfolding depth(2)[symmetric] unfolding d using fin 
    by (meson bdd_above_Maximum_nat bdd_above_nat image_iff)
  thus ?thesis unfolding max_depth_sort_def depth(1)[symmetric] using t
    by (intro exI[of _ t], auto)
qed

lemma max_depth_sort_Fun: assumes f: "f : σs → s in C" 
  and si: "si ∈ set σs" 
  and fins: "finite_sort C s" 
shows "max_depth_sort si < max_depth_sort s" 
proof -
  from C_sub_S[OF f] si have s: "s ∈ S" and siS: "si ∈ S" by auto
  from finite_arg_sort[OF fins f si] 
  have "finite_sort C si" .
  from max_depth_sort_wit[OF this siS] obtain ti where
    ti: "ti : si in 𝒯(C)" and depi: "depth_gterm ti = max_depth_sort si" by auto
  define t where "t s = (SOME t. t : s in 𝒯(C))" for s
  have t: "s ∈ set σs ⟹ t s : s in 𝒯(C)" for s 
    using someI_ex[OF sorts_non_empty[of s]] C_sub_S[OF f] 
    unfolding t_def by auto
  from si obtain i where si: "si = σs ! i" and i: "i < length σs" by (auto simp: set_conv_nth)
  define trm where "trm = Fun f (map (λ j. if j = i then ti else t (σs ! j)) [0..<length σs])"
  have trm: "trm : s in 𝒯(C)" 
    unfolding trm_def
    apply (intro Fun_hastypeI[OF f] list_all2_all_nthI)
     apply force
    subgoal for j using t si ti by (auto simp: set_conv_nth)
    done
  have "max_depth_sort si = depth_gterm ti" using depi by auto
  also have "… < depth_gterm trm" unfolding trm_def
    by (rule depth_gterm_arg, insert i, auto)
  also have "… ≤ max_depth_sort s" 
    using max_depth_sort_wit[OF fins s] trm by auto
  finally show ?thesis .
qed

lemma max_depth_sort_var: assumes "t : s in 𝒯(C, 𝒱 |` SS)" 
  and "x ∈ vars t" 
  and "finite_sort C s" 
shows "max_depth_sort (snd x) ≤ max_depth_sort s" 
  using assms
proof (induct)
  case (Var y s)
  thus ?case by (auto simp: hastype_def restrict_map_def split: if_splits)
next
  case (Fun f ts σs τ)
  from Fun(4) obtain i where i: "i < length ts" and x: "x ∈ vars (ts ! i)" 
    by (auto simp: set_conv_nth)
  from i Fun(2) have mem: "σs ! i ∈ set σs" by (auto simp: set_conv_nth list_all2_conv_all_nth)
  from finite_arg_sort[OF Fun(5,1) mem] 
  have "finite_sort C (σs ! i)" .
  with Fun(3) i x have "max_depth_sort (snd x) ≤ max_depth_sort (σs ! i)" 
    by (auto simp: list_all2_conv_all_nth)
  with max_depth_sort_Fun[OF Fun(1) mem Fun(5)]
  show ?case by simp
qed

definition max_depth_sort_smp :: "('f,'s) simple_match_problem_ms ⇒ nat" where
  "max_depth_sort_smp mp = Max (insert 0 (max_depth_sort ` snd ` tvars_smp (mset2 mp)))"

definition max_depth_sort_p :: "('f,'s) simple_pat_problem_ms ⇒ nat" where
  "max_depth_sort_p p = sum_mset (image_mset max_depth_sort_smp p)" 

lemma max_depth_sort_p_add[simp]: "max_depth_sort_p (add_mset mp p) = 
  max_depth_sort_smp mp + max_depth_sort_p p" 
  unfolding max_depth_sort_p_def by simp

lemma finite_constructor_form_pat_add: "finite_constructor_form_pat (mset3 (add_mset mp p))
  = (finite_constructor_form_mp (mset2 mp) ∧ finite_constructor_form_pat (mset3 p))"
  unfolding finite_constructor_form_pat_def by auto

lemma mds_decrease_inst: assumes ft: "is_Fun t"
  and tau: "τ ∈ τs n x" 
  and mp: "mp = {#{#Var x, t#}#}" 
  and fin: "finite_constructor_form_mp (mset2 mp)" 
shows "max_depth_sort_smp mp > max_depth_sort_smp (image_mset (image_mset (λt. t ⋅ τ)) mp)" 
proof -
  from fin[unfolded finite_constructor_form_mp_def mp] obtain ι
    where fin: "finite_sort C ι" and x: "Var x : ι in 𝒯(C,𝒱 |` SS)" and t: "t : ι in 𝒯(C,𝒱 |` SS)" 
    by auto
  from x have iota: "ι = snd x" and xS: "snd x ∈ S" by (auto simp: hastype_def restrict_map_def split: if_splits)
  from ft obtain f ts where ft: "t = Fun f ts" by (cases t, auto)
  from t[unfolded ft Fun_hastype] obtain σs where f: "f : σs → ι in C" 
    and ts: "ts :⇩l σs in 𝒯(C,𝒱 |` SS)" 
    by auto
  {
    fix y
    assume "y ∈ vars t" 
    from this[unfolded ft] obtain ti where y: "y ∈ vars ti" and ti: "ti ∈ set ts" by auto
    from ti ts obtain σi where σi: "σi ∈ set σs" and ti: "ti : σi in 𝒯(C,𝒱 |` SS)" 
      unfolding list_all2_conv_all_nth set_conv_nth by force
    from max_depth_sort_var[OF ti y finite_arg_sort[OF fin f σi]]
    have "max_depth_sort (snd y) ≤ max_depth_sort σi" .
    also have "… < max_depth_sort (snd x)" 
      using max_depth_sort_Fun[OF f σi fin] iota by auto
    finally have "max_depth_sort (snd y) < max_depth_sort (snd x)" by auto
  } note max_x = this

  from max_depth_sort_wit[OF fin, unfolded iota, OF xS] obtain wx
    where wx: "wx : snd x in 𝒯(C)" and to_wx: "max_depth_sort (snd x) = depth_gterm wx" 
      and wx_max: "⋀ t'. t' : snd x in 𝒯(C) ⟹ depth_gterm t' ≤ depth_gterm wx" by auto
      
  have "max_depth_sort_smp mp = Max (max_depth_sort ` snd ` insert x (vars t))" unfolding mp
    max_depth_sort_smp_def by auto
  also have "… = max_depth_sort (snd x)" 
    by (rule Max_eqI, insert max_x, force+)
  finally have max_mp: "max_depth_sort_smp mp = max_depth_sort (snd x)" .

  from tau[unfolded τs_def] obtain f σs where f: "f : σs → snd x in C" 
    and tau: "τ = τc n x (f,σs)" by auto
  have "max_depth_sort_smp (image_mset (image_mset (λt. t ⋅ τ)) mp) = 
     Max (insert 0 (max_depth_sort ` snd ` (vars (τ x) ∪ vars (t ⋅ τ))))" 
    unfolding max_depth_sort_smp_def mp by simp
  also have "… ≤ Max (insert 0 (max_depth_sort ` (snd ` vars (τ x) ∪ snd ` vars t)))" 
    by (rule Max_mono, auto simp: vars_term_subst tau τc_def subst_def)
  also have "snd ` vars (τ x) = set σs" unfolding tau τc_def subst_def 
    by (force simp: set_zip set_conv_nth[of σs])
  also have "Max (insert 0 (max_depth_sort ` (set σs ∪ snd ` vars t))) < max_depth_sort (snd x)"
  proof (subst Max_less_iff, force, force, intro ballI)
    fix d
    assume d: "d ∈ insert 0 (max_depth_sort ` (set σs ∪ snd ` vars t))" 
    show "d < max_depth_sort (snd x)" 
    proof (cases "d ∈ max_depth_sort ` snd ` vars t")
      case True
      with max_x show ?thesis by auto
    next
      case False
      hence "d = 0 ∨ d ∈ max_depth_sort ` set σs" using d by auto
      thus ?thesis
      proof
        assume "d = 0" 
        thus ?thesis unfolding to_wx by (cases wx, auto)
      next
        assume "d ∈ max_depth_sort ` set σs" 
        then obtain σ where mem: "σ ∈ set σs" and d: "d = max_depth_sort σ" by auto
        from max_depth_sort_Fun[OF f mem] d fin iota show ?thesis by auto
      qed
    qed
  qed
  finally show ?thesis unfolding max_mp .
qed
  
lemma mds_weak_decrease_inst: assumes tau: "τ ∈ τs n x" 
  and fin: "finite_sort C (snd x)" 
shows "max_depth_sort_smp mp ≥ max_depth_sort_smp (image_mset (image_mset (λt. t ⋅ τ)) mp)" 
proof -
  from tau[unfolded τs_def] obtain f σs where f: "f : σs → snd x in C" 
    and tau: "τ = τc n x (f,σs)" by auto
  note tau = tau[unfolded τc_def split]
  show ?thesis
  proof (cases "x ∈ tvars_smp (mset2 mp)")
    case False
    have "image_mset (image_mset (λt. t ⋅ τ)) mp = image_mset (image_mset (λ t. t ⋅ Var)) mp" 
    proof (intro image_mset_cong refl term_subst_eq, goal_cases)
      case (1 eqc t y)
      with False have "x ≠ y" by auto
      thus ?case unfolding tau by (auto simp: subst_def)
    qed 
    also have "… = mp" by simp
    finally show ?thesis by simp
  next
    case True
    define tv where "tv = tvars_smp (mset2 mp)" 
    let ?mp = "image_mset (image_mset (λt. t ⋅ τ)) mp" 
    from True have x: "x ∈ tv" unfolding tv_def .
    have fin: "finite tv" unfolding tv_def by auto
    have "max_depth_sort_smp mp = Max (insert 0 (max_depth_sort ` snd ` (insert x tv)))" 
      unfolding max_depth_sort_smp_def tv_def using True by auto
    also have "… = Max (max_depth_sort ` snd ` (insert x tv))" using fin by simp
    finally have max_mp: "max_depth_sort_smp mp = Max (max_depth_sort ` snd ` insert x tv)" .

    have "tvars_smp (mset2 ?mp) = ⋃ (vars ` τ ` tv)"
      by (fastforce simp add: tv_def vars_term_subst)
    also have "… = vars (τ x) ∪ ⋃ (vars ` τ ` tv)" using x by auto
    also have "… = vars (τ x) ∪ (tv - {x})" unfolding tau subst_def by auto
    finally have tvars: "tvars_smp (mset2 ?mp) = vars (τ x) ∪ (tv - {x})" .
      
    have "max_depth_sort_smp ?mp = Max (insert 0 (max_depth_sort ` (snd ` vars (τ x) ∪ snd ` (tv - {x}))))"
      unfolding max_depth_sort_smp_def tvars by (metis image_Un)
    also have "snd ` vars (τ x) = set σs" unfolding tau subst_def 
      by (force simp: set_zip set_conv_nth[of σs])
    also have "Max (insert 0 (max_depth_sort ` (set σs ∪ snd ` (tv - {x})))) 
       ≤ max_depth_sort_smp mp" unfolding max_mp
    proof (intro Max_le_MaxI)
      fix d
      assume d: "d ∈ insert 0 (max_depth_sort ` (set σs ∪ snd ` (tv - {x})))" 
      show "∃d'∈max_depth_sort ` snd ` insert x tv. d ≤ d'"
      proof (cases "d ∈ max_depth_sort ` set σs")
        case True
        then obtain σ where mem: "σ ∈ set σs" and d: "d = max_depth_sort σ" by auto
        from max_depth_sort_Fun[OF f mem assms(2)]
        show ?thesis unfolding d by auto
      qed (insert d, auto)
    qed (insert fin, auto)
    finally show ?thesis .
  qed
qed

lemma max_depth_sort_le: assumes "tvars_smp (mset2 mp) ⊆ tvars_smp (mset2 mp')"
  shows "max_depth_sort_smp mp ≤ max_depth_sort_smp mp'"
  unfolding max_depth_sort_smp_def
  apply (rule Max_le_MaxI)
     apply force
    apply force
   apply force
  using assms by auto

lemma mp_step_tvars: "mp →⇩s⇩s mp' ⟹ tvars_smp (mset2 mp') ⊆ tvars_smp (mset2 mp)"
proof (induct rule: smp_step_ms.induct)
  case *: (smp_decomp eqc f n eqcn mp)
  from *(2) show ?case 
  proof (clarsimp, goal_cases)
    case (1 x s i ti)
    from *(1)[OF 1(4)] 1(2,3)
    show ?case by (intro bexI[OF _ 1(4)], cases ti, auto)
  qed
qed auto

lemma max_depth_sort_p_inst: assumes mem: "{#{#Var x, t#}#} ∈# p" 
  and t: "is_Fun t" 
  and tau: "τ ∈ τs n x" 
  and fin: "finite_constructor_form_pat (mset3 p)"
shows "max_depth_sort_p p > max_depth_sort_p (image_mset (image_mset (image_mset (λt. t ⋅ τ))) p)" 
proof -
  obtain mp p' where p: "p = add_mset mp p'" and mp: "mp = {#{#Var x, t#}#}" 
    using mset_add[OF mem, of thesis] by simp
  from fin[unfolded finite_constructor_form_pat_def p]
  have fin: "finite_constructor_form_mp (mset2 mp)" by auto
  show ?thesis unfolding p
  proof (simp add: max_depth_sort_p_def image_mset.compositionality o_def)
    show "max_depth_sort_smp (image_mset (image_mset (λt. t ⋅ τ)) mp) +
      (∑x∈#p'. max_depth_sort_smp (image_mset (image_mset (λt. t ⋅ τ)) x))
    < max_depth_sort_smp mp + ∑⇩# (image_mset max_depth_sort_smp p')" (is "?a1 + ?b1 < ?a2 + ?b2")
    proof (rule add_less_le_mono)
      show "?a1 < ?a2" 
        by (rule mds_decrease_inst[OF t tau mp fin])
      show "?b1 ≤ ?b2" 
      proof (rule sum_mset_mono, rule mds_weak_decrease_inst[OF tau])
        from fin[unfolded finite_constructor_form_mp_def mp] obtain ι
          where fin: "finite_sort C ι" and x: "Var x : ι in 𝒯(C,𝒱 |` SS)" 
          by auto
        from x fin show "finite_sort C (snd x)" 
          by (auto simp: hastype_def restrict_map_def split: if_splits)
      qed
    qed
  qed
qed

lemma depth_gterm_le_card: "finite_sort C σ ⟹ t : σ in 𝒯(D) ⟹ D ⊆⇩m C ⟹ depth_gterm t ≤ card (dom D)"
proof (induct t arbitrary: σ D)
  case *: (Fun f ts σ D)
  from *(3)[unfolded Fun_hastype] obtain σs where f: "f : σs → σ in D" and ts: "ts :⇩l σs in 𝒯(D)" by auto
  from *(4) have "dom D ⊆ dom C" by (rule map_le_implies_dom_le)
  with finite_C have fin: "finite (dom D)" by (metis finite_subset)
  from f have mem: "(f,σs) ∈ dom D" by auto
  define domD' where "domD' = dom D - {(f,σs)}" 
  define D' where "D' = D |` domD'" 
  have dom: "dom D = insert (f,σs) (dom D')" unfolding D'_def domD'_def using mem by auto
  from arg_cong[OF this, of card] 
  have cardD: "card (dom D) = Suc (card (dom D'))" 
    unfolding D'_def domD'_def using mem fin by auto
  from f *(4) have "f : σs → σ in C" by (metis subssigD)
  hence sig: "σ ∈ S" using C_sub_S by blast
  show ?case 
  proof (cases ts)  
    case Nil
    thus ?thesis unfolding cardD by simp
  next
    case (Cons t ts')
    hence "map depth_gterm ts ≠ []" by auto
    from max_list_mem[OF this] obtain t where t: "t ∈ set ts" 
      and "max_list (map depth_gterm ts) = depth_gterm t" by auto
    hence depth: "depth_gterm (Fun f ts) = Suc (depth_gterm t)" by simp
    note IH = *(1)[OF t]
    have "D' ⊆⇩m C" using *(4) unfolding D'_def
      using map_le_trans by blast
    note IH = IH[OF _ _ this]
    from t ts obtain τ where tau: "τ ∈ set σs" and tt: "t : τ in 𝒯(D)" 
      by (force simp: list_all2_conv_all_nth set_conv_nth)
    have "f : σs → σ in C" by fact
    from finite_arg_sort[OF *(2) this tau] have "finite_sort C τ" by auto
    note IH = IH[OF this]
    have "t : τ in 𝒯(D')" 
    proof (rule ccontr)
      assume "¬ ?thesis" 
      from tt this have "∃ s. t ⊵ s ∧ s : σ in 𝒯(D)" 
      proof induct
        case (Fun g ss τs τ)
        show ?case
        proof (cases "ss :⇩l τs in 𝒯(D')")
          case True
          from this Fun(4) have "¬ (g : τs → τ in D')" 
            by (metis Fun_hastypeI)
          with Fun(1) have "(g,τs) = (f,σs)" unfolding D'_def domD'_def 
            by (auto simp: restrict_map_def fun_hastype_def hastype_def split: if_splits)
          with Fun(1) f have "τ = σ" by (simp add: fun_has_same_type)
          from Fun(1,2)[unfolded this] have "Fun g ss : σ in 𝒯(D)" by (rule Fun_hastypeI)
          thus ?thesis by blast
        next
          case False
          with Fun(2) obtain i where i: "i < length ss"
            and ssi: "¬ (ss ! i : τs ! i in 𝒯(D'))"
            by (force simp: list_all2_conv_all_nth set_conv_nth)
          from list_all2_nthD[OF Fun(3) i, rule_format, OF ssi]
          obtain s where "s ⊴ ss ! i" and s: "s : σ in 𝒯(D)" 
            by auto
          show ?thesis
          proof (intro exI[of _ s] conjI s)
            have "s ⊴ ss ! i" by fact
            also have "ss ! i ⊴ Fun g ss" using i by simp
            finally show "s ⊴ Fun g ss" by auto
          qed
        qed
      qed auto
      then obtain s where "s ⊴ t" and s: "s : σ in 𝒯(D)" by auto
      with t have sub: "Fun f ts ⊳ s" by auto
      from s *(4) have s: "s : σ in 𝒯(C)" by (metis hastype_in_Term_mono_left)
      from *(3,4) have t: "Fun f ts : σ in 𝒯(C)" by (metis hastype_in_Term_mono_left)
      from sub obtain c where "c ≠ □" and "Fun f ts = c ⟨s⟩" by blast
      from apply_ctxt_hastype_imp_hastype_context[OF t[unfolded this] s] 
      have c: "c : σ → σ in 𝒞(C,λx. None)" by auto
      from max_depth_sort_wit[OF *(2) sig]
      obtain t where t: "t : σ in 𝒯(C)" and large: "⋀ t'. t' : σ in 𝒯(C) ⟹ depth_gterm t' ≤ depth_gterm t" 
        by auto
      from t c have "c ⟨ t ⟩ : σ in 𝒯(C)" by (metis apply_ctxt_hastype)
      from large[OF this] have contra: "depth_gterm (c ⟨t⟩) ≤ depth_gterm t" .
      from ‹c ≠ □› obtain f bef d aft where c: "c = More f bef d aft" by (cases c, auto)
      have "depth_gterm t ≤ depth_gterm (d ⟨t⟩)" 
      proof (induct d)
        case (More f bef d aft)
        thus ?case using max_list[of "depth_gterm (d⟨t⟩)" "map depth_gterm bef @ depth_gterm d⟨t⟩ # map depth_gterm aft"] 
          by auto
      qed auto
      also have "… < depth_gterm (c ⟨t⟩)" unfolding c 
        using max_list[of "depth_gterm (d⟨t⟩)" "map depth_gterm bef @ depth_gterm d⟨t⟩ # map depth_gterm aft"] 
        by auto
      also have "… ≤ depth_gterm t" by (rule contra)
      finally show False by simp 
    qed
    from IH[OF this] show ?thesis unfolding depth cardD by auto
  qed
qed auto


lemma max_depth_sort_smp_le_card: assumes "finite_constructor_form_mp (mset2 mp)"
  shows "max_depth_sort_smp mp ≤ card (dom C)" 
  unfolding max_depth_sort_smp_def
proof (subst Max_le_iff, force intro!: finite_imageI, force, intro ballI)
  fix d
  assume d: "d ∈ insert 0 (max_depth_sort ` snd ` ⋃ (⋃ ((`) vars ` mset2 mp)))" 
  show "d ≤ card (dom C)" 
  proof (cases "d = 0")
    case False
    with d obtain eqc t x where "eqc ∈ mset2 mp" "t ∈ eqc" and 
      x: "x ∈ vars t" and d: "d = max_depth_sort (snd x)" 
      by blast
    with assms[unfolded finite_constructor_form_mp_def] obtain ι where fin: "finite_sort C ι" 
      and t: "t : ι in 𝒯(C,𝒱 |` SS)" by force
    define σ where "σ = snd x" 
    from t x have inS: "σ ∈ S" 
      by induct (auto simp: restrict_map_def hastype_def list_all2_conv_all_nth set_conv_nth 
          σ_def split: if_splits)
    from t fin x have fin: "finite_sort C σ"
    proof (induct)
      case (Var v σ)
      then show ?case by (auto simp: restrict_map_def hastype_def σ_def split: if_splits)
    next
      case *: (Fun f ss σs τ)
      from finite_arg_sort[OF *(4,1)] *(2,3,5)
      show ?case by (auto simp: list_all2_conv_all_nth set_conv_nth)
    qed
    from max_depth_sort_wit[OF this inS, folded d[folded σ_def]]
    obtain t where tσ: "t : σ in 𝒯(C)" "depth_gterm t = d" 
      "⋀ t'. t' : σ in 𝒯(C) ⟹ depth_gterm t' ≤ d" by auto
    from depth_gterm_le_card[OF fin tσ(1), unfolded tσ] show ?thesis by simp
  qed auto
qed 

lemma max_depth_sort_p_le_card_size: assumes "finite_constructor_form_pat (mset3 p)"
  shows "max_depth_sort_p p ≤ card (dom C) * size p" 
proof -
  have "max_depth_sort_p p = sum_mset (image_mset max_depth_sort_smp p)" unfolding max_depth_sort_p_def ..
  also have "… ≤ sum_mset (image_mset (λ mp. card (dom C)) p)" 
    by (rule sum_mset_mono, rule max_depth_sort_smp_le_card, 
      insert assms, auto simp: finite_constructor_form_pat_def)
  finally show ?thesis by (simp add: ac_simps)
qed


definition num_syms_smp :: "('f,'s)simple_match_problem_ms ⇒ nat" where
  "num_syms_smp mp = sum_mset (image_mset num_syms (sum_mset mp))" 

lemma num_syms_subset: assumes "sum_mset mp ⊂# sum_mset mp'" 
  shows "num_syms_smp mp < num_syms_smp mp'"
proof -
  from assms obtain ts where "sum_mset mp' = ts + sum_mset mp" and "ts ≠ {#}" 
    by (metis add.commute subset_mset.lessE)
  thus ?thesis unfolding num_syms_smp_def 
    by (cases ts, auto)
qed

definition max_dupl_smp where
  "max_dupl_smp mp = Max (insert 0 ((λ x. (∑ t∈# sum_mset mp. count (syms_term t) (Inl x))) ` tvars_smp (mset2 mp)))" 

definition max_dupl_p :: "('f,'s)simple_pat_problem_ms ⇒ nat" where
  "max_dupl_p p = sum_mset (image_mset max_dupl_smp p)" 


lemma max_dupl_smp: "(∑ t∈# sum_mset mp. count (syms_term t) (Inl x)) ≤ max_dupl_smp mp" 
proof (cases "x ∈ tvars_smp (mset2 mp)")
  case True
  thus ?thesis unfolding max_dupl_smp_def
    by (intro Max_ge[OF finite.insertI[OF finite_imageI]], auto)
next
  case False
  have "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) = 0" 
  proof (clarsimp)
    fix eq t
    assume "eq ∈# mp" "t ∈# eq" 
    with False have "x ∉ vars t" by auto
    thus "count (syms_term t) (Inl x) = 0" unfolding vars_term_syms_term
      by (simp add: count_eq_zero_iff)
  qed
  thus ?thesis by linarith
qed

lemma max_dupl_smp_le_num_syms: "max_dupl_smp mp ≤ num_syms_smp mp" 
  unfolding max_dupl_smp_def
proof (subst Max_le_iff, force intro!: finite_imageI simp: tvars_match_def, force, intro ballI)
  fix n
  assume n: "n ∈ insert 0 {∑t∈#∑⇩# mp. count (syms_term t) (Inl x) |. x ∈ tvars_smp (mset2 mp)}" 
  show "n ≤ num_syms_smp mp" 
  proof (cases "n = 0")
    case False
    with n obtain x where x: "x ∈ tvars_smp (mset2 mp)" 
      and n: "n = (∑t∈#∑⇩# mp. count (syms_term t) (Inl x))" by auto
    have nt: "num_syms_smp mp = ∑⇩# (image_mset num_syms (∑⇩# mp))" 
      unfolding num_syms_smp_def ..
    show ?thesis unfolding n nt
    proof (rule sum_mset_mono, goal_cases)
      case (1 t)
      show "count (syms_term t) (Inl x) ≤ num_syms t" 
        unfolding num_syms_def by (rule count_le_size)
    qed
  qed auto
qed 

lemma num_syms_smp_τs: assumes τ: "τ ∈ τs n x"
  shows "num_syms_smp (image_mset (image_mset (λt. t ⋅ τ)) mp) ≤ num_syms_smp mp + max_dupl_smp mp * m" 
proof - 
  have "num_syms_smp (image_mset (image_mset (λt. t ⋅ τ)) mp) = 
    (∑ eq∈#mp. (∑ t∈#eq. num_syms (t ⋅ τ)))" 
    unfolding num_syms_smp_def image_mset.compositionality o_def
    by (induct mp, auto simp: image_mset.compositionality o_def)
  also have "… ≤ (∑ eq∈#mp. (∑ t∈#eq. num_syms t + count (syms_term t) (Inl x) * m))" 
    using num_syms_τs[OF τ] 
    by (intro sum_mset_mono, auto)
  also have "… = (∑ eq∈#mp. (∑ t∈#eq. num_syms t)) + (∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x) * m))" 
    unfolding sum_mset.distrib by simp
  also have "(∑ eq∈#mp. (∑ t∈#eq. num_syms t)) = num_syms_smp mp" 
    unfolding num_syms_smp_def by (induct mp, auto)
  also have "(∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x) * m))
     = (∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x))) * m" 
    unfolding sum_mset_distrib_right by simp
  also have "(∑ eq∈#mp. (∑ t∈#eq. count (syms_term t) (Inl x)))
     = (∑ t∈# sum_mset mp. count (syms_term t) (Inl x))" 
    by (induct mp, auto)
  also have "… * m ≤ max_dupl_smp mp * m" 
    using max_dupl_smp[of x mp] by simp
  finally show ?thesis by simp
qed

lemma max_dupl_smp_τs: assumes τ: "τ ∈ τs n x"
    and disj: "fst ` tvars_smp (mset2 mp) ∩ {n..<n + m} = {}" 
  shows "max_dupl_smp (image_mset (image_mset (λt. t ⋅ τ)) mp) ≤ max_dupl_smp mp" 
proof - 
  from τ[unfolded τs_def] obtain f ss 
    where f: "f : ss → snd x in C" and τ: "τ = τc n x (f,ss)" by auto
  define vs where "vs = (zip [n..<n + length ss] ss)" 
  define s where "s = (Fun f (map Var vs))" 
  have tau: "τ = subst x s" unfolding τ τc_def s_def vs_def by auto
  show ?thesis
  proof (cases "x ∈ tvars_smp (mset2 mp)")
    case False
    have "image_mset (image_mset (λt. t ⋅ τ)) mp = image_mset (image_mset (λt. t ⋅ Var)) mp" 
    proof (intro image_mset_cong term_subst_eq, goal_cases)
      case (1 eq t y)
      with False show ?case by (auto simp: tau subst_def)
    qed
    thus ?thesis by simp
  next
    case x: True
    show ?thesis unfolding max_dupl_smp_def
    proof ((intro Max_le_MaxI; (intro finite.insertI, force)?), force, goal_cases)
      case (1 d)
      show ?case
      proof (cases "d = 0")
        case False
        with 1 obtain y where 
          d: "d = (∑t∈#∑⇩# (image_mset (image_mset (λt. t ⋅ τ)) mp). count (syms_term t) (Inl y))" 
          and y: "y ∈ tvars_smp (mset2 (image_mset (image_mset (λt. t ⋅ τ)) mp))" by auto
        have syms_s: "syms_term s = add_mset (Inr f) (mset (map Inl vs))" unfolding s_def
          by (simp, induct vs, auto)
        define repl :: "('f, nat × 's) Term.term ⇒ (nat × 's + 'f) multiset"  
          where "repl t = replicate_mset (count (syms_term t) (Inl x)) (Inl x)" for t
        let ?add = "(∑t∈#∑⇩# mp. count (repl t) (Inl y))" 
        let ?symsy = "(∑t∈#∑⇩# mp. count (syms_term t) (Inl y))" 
        let ?symsxy = "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x) * count (syms_term s) (Inl y))" 
        let ?symsx = "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x))" 
        have "d = (∑t∈#∑⇩# mp. count (syms_term (t ⋅ τ)) (Inl y))" 
          unfolding d
        proof (induct mp, auto, goal_cases)
          case (1 eq mp)
          show ?case by (induct eq, auto)
        qed
        also have "… ≤ … + ?add" by simp
        also have "… = 
           (∑t∈#∑⇩# mp. count (syms_term (t ⋅ τ) + repl t) (Inl y))" 
          unfolding sum_mset.distrib[symmetric]
          by (rule arg_cong[of _ _ sum_mset], rule image_mset_cong, simp)
        also have "… = ?symsy + ?symsxy" 
          unfolding repl_def tau syms_term_subst sum_mset.distrib[symmetric] by simp
        finally have d: "d ≤ ?symsy + ?symsxy" .
        show ?thesis
        proof (cases "y ∈ set vs")
          case False
          hence "?symsxy = 0" unfolding syms_s by auto
          with d have d: "d ≤ ?symsy" by auto
          from y[simplified] obtain eq t 
            where eq: "eq ∈# mp" and t: "t ∈# eq" and y: "y ∈ vars (t ⋅ τ)" 
            by auto
          from False this[unfolded vars_term_subst tau subst_def s_def]
          have "y ∈ vars t" by (auto split: if_splits)
          hence "y ∈ tvars_smp (mset2 mp)" using eq t by auto
          with d show ?thesis by auto
        next
          case True
          have dist: "distinct vs" unfolding vs_def
            by (metis distinct_enumerate enumerate_eq_zip)
          from split_list[OF True] obtain vs1 vs2 where vs: "vs = vs1 @ y # vs2" by auto
          with dist have nmem: "y ∉ set vs1" "y ∉ set vs2" by auto
          have "count (syms_term s) (Inl y) = 1" unfolding syms_s vs using nmem
            by (auto simp: count_eq_zero_iff) 
          with d have d: "d ≤ ?symsy + ?symsx" by auto
          from True have "fst y ∈ {n..<n + m}" unfolding vs_def using m[OF f] 
            by (auto simp: set_zip)
          with disj have "y ∉ tvars_smp (mset2 mp)" by blast
          hence "?symsy = 0" 
            by (auto simp: count_eq_zero_iff vars_term_syms_term)
          with d have "d ≤ ?symsx" by auto
          with x show ?thesis by auto
        qed
      qed auto
    qed
  qed
qed


definition num_syms_p :: "('f,'s)simple_pat_problem_ms ⇒ nat" where
  "num_syms_p p = sum_mset (image_mset num_syms_smp p)" 

lemma num_syms_p_add[simp]: "num_syms_p (add_mset mp p) = num_syms_smp mp + num_syms_p p" 
  unfolding num_syms_p_def by simp

lemma max_dupl_p_le_num_syms: "max_dupl_p p ≤ num_syms_p p"
  unfolding max_dupl_p_def num_syms_p_def
  by (rule sum_mset_mono[OF max_dupl_smp_le_num_syms])

lemma max_dupl_p_add[simp]: "max_dupl_p (add_mset mp p) = max_dupl_smp mp + max_dupl_p p" 
  unfolding max_dupl_p_def by simp

lemma max_dupl_mono_main: assumes "⋀ x. (∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) ≤ (∑t∈#∑⇩# mp'. count (syms_term t) (Inl x))" 
  and "tvars_smp (mset2 mp) ⊆ tvars_smp (mset2 mp')" 
shows "max_dupl_smp mp ≤ max_dupl_smp mp'" 
  unfolding max_dupl_smp_def
proof ((intro Max_le_MaxI; (intro finite.insertI, force)?), force, goal_cases)
  case (1 d)
  show ?case
  proof (cases "d = 0")
    case False
    with 1 obtain x where d: "d = (∑t∈#∑⇩# mp. count (syms_term t) (Inl x))" 
      and x: "x ∈ tvars_smp (mset2 mp)" by auto
    with x assms(2) have x: "x ∈ tvars_smp (mset2 mp')" by blast
    define d' where "d' = (∑t∈#∑⇩# mp'. count (syms_term t) (Inl x))"  
    have "d ≤ d'" unfolding d d'_def by fact
    with x show ?thesis unfolding d'_def by blast
  qed auto
qed


lemma max_dupl_mono: assumes "sum_mset mp ⊆# sum_mset mp'"
  shows "max_dupl_smp mp ≤ max_dupl_smp mp'" 
proof (rule max_dupl_mono_main)
  from set_mp[OF set_mset_mono[OF assms]] 
  show "tvars_smp (mset2 mp) ⊆ tvars_smp (mset2 mp')" by force
  from assms obtain mp2 where eq: "sum_mset mp' = sum_mset mp + mp2" by (rule subset_mset.less_eqE) 
  fix x
  show "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) ≤ (∑t∈#∑⇩# mp'. count (syms_term t) (Inl x))" 
    unfolding eq image_mset_union by auto
qed  


definition syms_smp :: "('f,'s)simple_match_problem_ms ⇒ (nat × 's + 'f) multiset" where
  "syms_smp mp = sum_mset (image_mset syms_term (sum_mset mp))" 

definition syms_eqc :: "('f,nat × 's)term multiset ⇒ (nat × 's + 'f) multiset" where
  "syms_eqc eqc = sum_mset (image_mset syms_term eqc)" 

lemma syms_smp_to_eqc: "syms_smp mp = sum_mset (image_mset syms_eqc mp)" 
  unfolding syms_smp_def syms_eqc_def 
  by (induct mp, auto)

lemma nums_eq_size_syms_smp: "num_syms_smp mp = size (syms_smp mp)" 
  unfolding num_syms_smp_def syms_smp_def num_syms_def 
proof (induct mp)
  case (add eq mp)
  show ?case
    apply (simp add: add)
    apply (induct eq, auto)
    done
qed auto

lemma num_syms_sym_subset: assumes "syms_smp mp ⊂# syms_smp mp'" 
  shows "num_syms_smp mp < num_syms_smp mp'" 
proof -
  from assms obtain d where mp': "syms_smp mp' = d + syms_smp mp" and d: "d ≠ {#}"
    by (metis add.commute subset_mset.lessE)
  thus ?thesis unfolding nums_eq_size_syms_smp by (cases d, auto)
qed

lemma num_syms_smp_step: "mp →⇩s⇩s mp' ⟹ finite_constructor_form_mp (mset2 mp) 
  ⟹ num_syms_smp mp' < num_syms_smp mp" 
proof (induct rule: smp_step_ms.induct)
  case (smp_dup t eqc mp)
  show ?case by (rule num_syms_subset, auto)
next
  case (smp_singleton t mp)
  show ?case by (rule num_syms_subset, auto)
next
  case (smp_triv_sort t ι eq mp)
  show ?case by (rule num_syms_subset, auto)
next
  case *: (smp_decomp eqc f n eqcn mp)
  define nums where "nums = mset_set {0..<n}" 
  from *(4) have eqc: "eqc ≠ {#}" unfolding finite_constructor_form_mp_def by auto
  define arg where "arg t = (∑i∈#nums. syms_term (args t ! i))" for t :: "('f, nat × 's) term" 
  {
    fix t
    assume "t ∈# eqc" 
    from *(1)[OF this] obtain ts where t: "t = Fun f ts" and len: "n = length ts" by (cases t, auto)
    have id: "mset ts = image_mset ((!) ts) (mset [0..<length ts])" 
      by (metis map_nth' mset_map)
    have "syms_term t = add_mset (Inr f) (arg t)" unfolding t arg_def nums_def len
      by (auto simp: id image_mset.compositionality o_def)
  } note step = this
  have "?case ⟷ num_syms_smp eqcn < num_syms_smp {#eqc#}" using * unfolding num_syms_smp_def by auto
  also have …
  proof (rule num_syms_sym_subset)
    from eqc obtain t eqc' where eqc: "eqc = add_mset t eqc'" by (cases eqc, auto)
    have "syms_smp eqcn = (∑i∈#nums. syms_eqc {#args t ! i. t ∈# eqc#})" 
      unfolding  image_mset.compositionality o_def nums_def syms_smp_to_eqc *(2)
      by simp
    also have "… = (∑t∈#eqc. arg t)" unfolding arg_def
      unfolding syms_eqc_def image_mset.compositionality o_def 
      by (rule sum_mset.swap)
    also have "… = arg t + (∑t∈#eqc'. arg t)" unfolding eqc by auto
    also have "… ⊂# syms_term t + (∑t∈#eqc'. syms_term t)" 
    proof (rule subset_mset.add_less_le_mono)
      from step[of t] eqc 
      show "arg t ⊂# syms_term t" by auto
      from step have step: "t ∈# eqc' ⟹ syms_term t = add_mset (Inr f) (arg t)" for t unfolding eqc by auto
      have "∑⇩# (image_mset syms_term eqc') = ∑⇩# (image_mset (λ t. add_mset (Inr f) (arg t)) eqc')"
        by (subst image_mset_cong[OF step], auto)
      also have "… = ∑⇩# (image_mset (λ t. arg t) eqc') + image_mset (λ t. Inr f) eqc'" 
        by (induct eqc', auto)
      finally 
      show "∑⇩# (image_mset arg eqc') ⊆# ∑⇩# (image_mset syms_term eqc')" by simp
    qed
    also have "syms_term t + (∑t∈#eqc'. syms_term t) = (∑t∈#eqc. syms_term t)" unfolding eqc by simp
    also have "… = syms_smp {#eqc#}" unfolding syms_smp_to_eqc syms_eqc_def by simp
    finally show "syms_smp eqcn ⊂# syms_smp {#eqc#}" .
  qed
  finally show ?case .
qed

lemma num_syms_smp_pos[simp]: assumes "finite_constructor_form_mp (mset2 mp)" 
  and "mp ≠ {#}" 
shows "num_syms_smp mp > 0" 
proof -
  from assms obtain eqc mp' where mp: "mp = add_mset eqc mp'" by (cases mp, auto)
  with assms have "eqc ≠ {#}" unfolding  finite_constructor_form_mp_def by auto
  thus ?thesis unfolding mp num_syms_smp_def by (cases eqc, auto)
qed

lemma count_syms_smp: "(∑t∈#∑⇩# mp. count (syms_term t) (Inl x)) = (count (syms_smp mp) (Inl x))" 
  unfolding syms_smp_def 
proof (induct mp, auto simp: image_mset.compositionality o_def, goal_cases)
  case (1 eq mp)
  show ?case by (induct eq, auto)
qed


lemma max_dupl_smp_step: "mp →⇩s⇩s mp' ⟹ max_dupl_smp mp' ≤ max_dupl_smp mp" 
proof (induct rule: smp_step_ms.induct)
  case (smp_dup t eqc mp)
  show ?case by (rule max_dupl_mono, auto)
next
  case (smp_singleton t mp)
  show ?case by (rule max_dupl_mono, auto)
next
  case (smp_triv_sort t ι eq mp)
  show ?case by (rule max_dupl_mono, auto)
next
  case *: (smp_decomp eqc f n eqcn mp)
  show ?case
  proof (rule max_dupl_mono_main, unfold count_syms_smp, rule mset_subset_eq_count)
    have "syms_smp eqcn ⊆# syms_smp {#eqc#}" 
    proof -
      define nums where "nums = mset_set {0..<n}" 
      define arg where "arg t = (∑i∈#nums. syms_term (args t ! i))" for t :: "('f, nat × 's) term" 
      have "syms_smp eqcn = (∑i∈#nums. syms_eqc {#args t ! i. t ∈# eqc#})" 
        unfolding  image_mset.compositionality o_def nums_def syms_smp_to_eqc *(2)
        by simp
      also have "… = (∑t∈#eqc. arg t)" unfolding arg_def
        unfolding syms_eqc_def image_mset.compositionality o_def 
        by (rule sum_mset.swap)
      finally have transform: "syms_smp eqcn = ∑⇩# (image_mset arg eqc)" .

      have "?thesis ⟷ ∑⇩# (image_mset arg eqc) ⊆# ∑⇩# (image_mset syms_term eqc)" 
        unfolding transform unfolding syms_smp_def by simp
      also have "…" 
      proof -
        {
          fix t
          assume "t ∈# eqc"
          from *(1)[OF this] obtain ts where t: "t = Fun f ts" and len: "length ts = n" by (cases t, auto)
          have id: "mset ts = mset (map (λ i. ts ! i) [0..< length ts])" 
            by (intro arg_cong[of _ _ mset], rule nth_equalityI, auto)
          have "arg t = (∑i∈#mset_set {0..<length ts}. syms_term (ts ! i))" 
            unfolding arg_def t nums_def len by simp
          also have "… = (∑⇩# (image_mset syms_term (mset ts)))" 
            unfolding id 
            by (auto simp: image_mset.compositionality o_def)
          finally have "arg t ⊆# syms_term t" unfolding t by simp
        }
        thus ?thesis 
          by (induct eqc, auto intro: subset_mset.add_mono)
      qed
      finally show ?thesis .
    qed 
    thus "syms_smp (eqcn + mp) ⊆# syms_smp (add_mset eqc mp)" 
      unfolding syms_smp_def by auto
 
    have "⋃ (⋃x∈set_mset eqcn. vars ` set_mset x) ⊆ ⋃ (vars ` set_mset eqc)" unfolding *(2)
    proof (clarsimp, goal_cases)
      case (1 x s i t)
      from *(1) 1 have "root t = Some (f,n)" by auto
      with 1 have "(x,s) ∈ vars t" by (cases t, auto)
      with 1 show ?case by auto
    qed
    thus "tvars_smp (mset2 (eqcn + mp)) ⊆ tvars_smp (mset2 (add_mset eqc mp))" 
      by force
  qed  
qed

definition measure_p :: "('f,'s) simple_pat_problem_ms ⇒ nat" where
  "measure_p p = max_depth_sort_p p * (max_dupl_p p * m + 1) + num_syms_p p" 

lemma measure_p_bound: assumes "finite_constructor_form_pat (mset3 p)" 
  shows "measure_p p ≤ card (dom C) * size p * (num_syms_p p + 1) * (m + 1)" 
proof -
  {
    assume "num_syms_p p ≠ 0" 
    from this[unfolded num_syms_p_def] obtain mp where mp: "mp ∈# p" and "num_syms_smp mp ≠ 0" by auto
    from this[unfolded num_syms_smp_def] obtain eqc t where eqc: "eqc ∈# mp" and t: "t ∈# eqc" and "num_syms t ≠ 0" 
      by auto
    from assms mp have "finite_constructor_form_mp (mset2 mp)" 
      by (auto simp: finite_constructor_form_pat_def)
    from this[unfolded finite_constructor_form_mp_def] eqc t obtain ι where "t : ι in 𝒯(C,𝒱 |` SS)" by auto
    hence "t ⋅ σg : ι in 𝒯(C)"
      by (metis σg' σg'_def σg_def sorted_map_cong subst_has_same_type)
    then obtain t where "t : ι in 𝒯(C)" by auto
    then obtain f where "f ∈ dom C" by (induct, auto simp: fun_hastype_def)
    hence "card (dom C) ≠ 0" "size p ≠ 0" using finite_C mp by auto 
  } note non_triv_p = this  
  have "measure_p p ≤ (card (dom C) * size p) * (num_syms_p p * m + 1) + num_syms_p p" 
    unfolding measure_p_def
    by (intro add_right_mono mult_mono max_dupl_p_le_num_syms max_depth_sort_p_le_card_size assms, auto)
  also have "… ≤ (card (dom C) * size p) * (num_syms_p p * m + 1) + (card (dom C) * size p) * num_syms_p p" 
  proof (cases "num_syms_p p = 0")
    case False
    from non_triv_p[OF this] have "card (dom C) * size p ≠ 0" by auto
    thus ?thesis by (cases "card (dom C) * size p", auto)
  qed auto
  also have "… = (card (dom C) * size p) * (num_syms_p p * m + 1 + num_syms_p p)" 
    by (simp add: algebra_simps)
  also have "… ≤ (card (dom C) * size p) * ((num_syms_p p + 1) * (m + 1))" 
    by (rule mult_left_mono, auto)
  finally show "measure_p p ≤ card (dom C) * size p * (num_syms_p p + 1) * (m + 1)" 
    by (simp add: algebra_simps)
qed 


lemma measure_p_num_syms: assumes "max_depth_sort_p p ≤ max_depth_sort_p p'" 
  and "max_dupl_p p ≤ max_dupl_p p'" 
  and "num_syms_p p < num_syms_p p'" 
shows "measure_p p < measure_p p'" 
  unfolding measure_p_def
  by (intro add_le_less_mono mult_mono, insert assms, auto)


lemma spp_step_complexity_and_termination: 
  assumes "p ⇒⇩s⇩s Pn" 
  and "finite_constructor_form_pat (mset3 p)" 
  and "pn ∈# Pn" 
shows "measure_p pn < measure_p p" 
  using assms
proof (induct)
  case *: (spp_simp mp mp' p)
  hence pn: "pn = add_mset mp' p" by simp
  let ?p = "add_mset mp p" 
  from * have fin: "finite_constructor_form_mp (mset2 mp)" 
    unfolding finite_constructor_form_pat_def by auto
  from num_syms_smp_step[OF *(1) fin]
  have n: "num_syms_p pn < num_syms_p ?p" unfolding pn by simp
  have d: "max_depth_sort_p pn ≤ max_depth_sort_p ?p" 
    unfolding pn
    apply simp
    apply (rule max_depth_sort_le)
    apply (rule mp_step_tvars)
    by fact
  from max_dupl_smp_step[OF *(1)] *
  have m: "max_dupl_p pn ≤ max_dupl_p ?p" by simp
  from d n m show ?case by (intro measure_p_num_syms, auto)
next
  case *: (spp_delete mp p)  
  hence pn: "pn = p" 
    and fin: "finite_constructor_form_mp (mset2 mp)" 
      unfolding finite_constructor_form_pat_def by auto
  let ?p = "add_mset mp p" 
  have d: "max_depth_sort_p pn ≤ max_depth_sort_p ?p" unfolding pn max_depth_sort_p_def by auto
  from *(1) have "mp ≠ {#}" by (cases, auto)
  from num_syms_smp_pos[OF fin this]
  have n: "num_syms_p pn < num_syms_p ?p" unfolding pn by simp
  have m: "max_dupl_p pn ≤ max_dupl_p ?p" unfolding pn by simp
  from d n m show ?case by (intro measure_p_num_syms, auto)
next
  case *: (spp_delete_large_sort n x ι eq mp t p)
  define pd where "pd = mset (map mp [0..<Suc n])" 
  from *(5) have pn: "pn = p" by auto
  let ?p = "p + pd" 
  have m: "max_dupl_p p ≤ max_dupl_p ?p" unfolding max_dupl_p_def by auto
  have d: "max_depth_sort_p p ≤ max_depth_sort_p ?p" unfolding max_depth_sort_p_def by auto
  have "num_syms_p p < num_syms_p p + 1" by auto
  also have "… ≤ num_syms_p p + num_syms_p pd"
  proof (rule add_left_mono)
    have mem: "mp n ∈# pd" unfolding pd_def by auto
    from *(4) have "finite_constructor_form_mp (mset2 (mp n))" 
      by (auto simp: finite_constructor_form_pat_def)
    from *(1)[OF le_refl] num_syms_smp_pos[OF this]
    have "1 ≤ num_syms_smp (mp n)" by (cases "mp n", auto)
    thus "1 ≤ num_syms_p pd" using mem unfolding num_syms_p_def
      by (metis One_nat_def add_eq_0_iff_both_eq_0 less_Suc0 linorder_not_less multi_member_split sum_mset.insert)
  qed
  finally have n: "num_syms_p p < num_syms_p ?p" unfolding num_syms_p_def by auto
  from n m d have "measure_p p < measure_p (p + pd)" by (metis measure_p_num_syms)
  thus ?case unfolding pn pd_def by auto
next
  case *: (spp_inst x t p n)
  then obtain τ where pn: "pn = image_mset (image_mset (image_mset (λt. t ⋅ τ))) p" 
    and τ: "τ ∈ τs n x" using τs_list by auto
  from max_depth_sort_p_inst[OF *(1-2) τ *(4)] *(5)
  have d: "max_depth_sort_p pn < max_depth_sort_p p" unfolding pn by auto
  have "num_syms_p pn = (∑mp∈#p. num_syms_smp (image_mset (image_mset (λt. t ⋅ τ)) mp))" 
    unfolding num_syms_p_def pn image_mset.compositionality o_def by simp
  also have "… ≤ (∑mp∈#p. num_syms_smp mp + max_dupl_smp mp * m)"
    by (rule sum_mset_mono, rule num_syms_smp_τs[OF τ])
  also have "… = num_syms_p p + max_dupl_p p * m" 
    unfolding sum_mset.distrib num_syms_p_def max_dupl_p_def sum_mset_distrib_right by auto
  finally have n: "num_syms_p pn ≤ num_syms_p p + max_dupl_p p * m" .
  have m: "max_dupl_p pn ≤ max_dupl_p p" 
    unfolding max_dupl_p_def pn image_mset.compositionality o_def
  proof (rule sum_mset_mono, rule max_dupl_smp_τs[OF τ], goal_cases)
    case (1 mp)
    thus ?case using *(3) by fastforce
  qed
  show ?case unfolding measure_p_def
    by (intro measure_expr_decrease n m d)
next
  case *: (spp_split mp x t eqc mp' p)
  let ?p = "add_mset mp p" 
  from *(1,5) have d: "max_depth_sort_p pn ≤ max_depth_sort_p ?p" 
    by (auto, auto intro!: max_depth_sort_le)
  from *(1,5) have m: "max_dupl_p pn ≤ max_dupl_p ?p" 
    by (auto, auto intro!: max_dupl_mono)
  have n: "num_syms_p pn < num_syms_p ?p"
  proof (cases eqc)
    case add
    from *(1,5) add
    show ?thesis by auto (auto intro!: num_syms_subset)
  next
    case empty
    with *(3) obtain eq2 mp2 where mp': "mp' = add_mset eq2 mp2" by (cases mp', auto)
    from *(1,4) mp' have eq2: "eq2 ≠ {#}" 
      unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def by auto
    from *(1,5) mp' eq2 
    show ?thesis by auto (cases eq2, auto intro!: num_syms_subset)
  qed
  from d n m show ?case by (intro measure_p_num_syms, auto)
qed auto

(* ************************************* 
     non-deterministic algorithm  
   ************************************* *)
text ‹snd = Simplified Non-Deterministic›
inductive_set snd_step :: "('f,'s)simple_pat_problem_ms rel" (‹⇒⇩s⇩n⇩d›)
  where snd_step: "p ⇒⇩s⇩s Q ⟹ finite_constructor_form_pat (mset3 p) ⟹ q ∈# Q ⟹ (p,q) ∈ ⇒⇩s⇩n⇩d" 

lemma snd_step_measure: assumes "(p,q) ∈ ⇒⇩s⇩n⇩d"
  shows "measure_p p > measure_p q"
  using assms
proof (cases)
  case (snd_step Q)
  thus ?thesis using spp_step_complexity_and_termination[of p Q q] by auto
qed

lemma snd_bound_steps: assumes "(p,q) ∈ ⇒⇩s⇩n⇩d ^^ n" 
  shows "measure_p q + n ≤ measure_p p" 
  using steps_bound[of "⇒⇩s⇩n⇩d" measure_p p q n, OF snd_step_measure assms]
  by auto

lemma snd_steps_bound: assumes steps: "(p,q) ∈ ⇒⇩s⇩n⇩d ^^ n" 
  and "finite_constructor_form_pat (mset3 p)" 
shows "n ≤ card (dom C) * size p * (num_syms_p p + 1) * (m + 1)" 
proof -
  from snd_bound_steps[OF steps] 
  have "n ≤ measure_p p" by auto
  also have "… ≤ card (dom C) * size p * (num_syms_p p + 1) * (m + 1)" 
    by (rule measure_p_bound[OF assms(2)])
  finally show ?thesis .
qed

lemma SN_snd_step: "SN ⇒⇩s⇩n⇩d" 
proof (rule SN_subset[OF SN_inv_image[OF SN_nat_gt]])
  show "⇒⇩s⇩n⇩d ⊆ inv_image {(a, b). b < a} measure_p" using snd_step_measure by auto
qed

lemma snd_step_size: assumes "(p,q) ∈ ⇒⇩s⇩n⇩d"
  shows "size p ≥ size q"
  using assms
proof (cases)
  case (snd_step Q)
  thus ?thesis using spp_step_ms_size[of p Q q] by auto
qed

lemma snd_step_finite_constructor_form_pat: assumes "(p,q) ∈ ⇒⇩s⇩n⇩d"
shows "finite_constructor_form_pat (mset3 q)" 
  using assms
proof (cases)
  case (snd_step Q)
  thus ?thesis using spp_step_ms[of p Q] by auto
qed

lemma snd_step_completeness: assumes "p ∉ NF ⇒⇩s⇩n⇩d" 
  shows "simple_pat_complete C SS (mset3 p) ⟷ (∀ q. (p,q) ∈ ⇒⇩s⇩n⇩d ⟶ simple_pat_complete C SS (mset3 q))"
  (is "?left = ?right")
proof -
  from assms obtain q where "(p,q) ∈ ⇒⇩s⇩n⇩d" by auto
  then obtain Q where "p ⇒⇩s⇩s Q" and fin: "finite_constructor_form_pat (mset3 p)" 
    by cases auto
  from spp_step_ms[OF this] snd_step[OF this]
  have oneDir: "?right ⟹ ?left" by auto
  {
    assume "¬ ?right" 
    then obtain q where "(p,q) ∈ ⇒⇩s⇩n⇩d" and not: "¬ simple_pat_complete C SS (mset3 q)" by auto
    from this(1) obtain Q where "p ⇒⇩s⇩s Q" and "q ∈# Q" by cases auto
    from spp_step_ms[OF this(1) fin] this(2) not
    have "¬ ?left" by auto
  }
  with oneDir show ?thesis by auto
qed

lemma snd_steps: assumes "(p,q) ∈ (⇒⇩s⇩n⇩d)⇧*" 
  shows "size p ≥ size q" 
  "simple_pat_complete C SS (mset3 p) ⟹ simple_pat_complete C SS (mset3 q)" 
  "finite_constructor_form_pat (mset3 p) ⟹ finite_constructor_form_pat (mset3 q)" 
  using assms
proof (atomize(full), induct, force)
  case (step q r)
  from step(2) have "q ∉ NF ⇒⇩s⇩n⇩d" by auto
  from snd_step_completeness[OF this] 
    snd_step_finite_constructor_form_pat[OF step(2)]
    snd_step_size[OF step(2)]
    step(2-3)
  show ?case by auto
qed

lemma snd_steps_complete: assumes "¬ simple_pat_complete C SS (mset3 p)"
  shows "∃ q. (p,q) ∈ ⇒⇩s⇩n⇩d⇧! ∧ ¬ simple_pat_complete C SS (mset3 q)" 
  using assms
proof (induct p rule: SN_induct[OF SN_snd_step])
  case (1 p)
  show ?case
  proof (cases "p ∈ NF ⇒⇩s⇩n⇩d")
    case True
    thus ?thesis using 1 by auto
  next
    case False
    from snd_step_completeness[OF False] 1 obtain q where step: "(p,q) ∈ ⇒⇩s⇩n⇩d" 
      and q: "¬ simple_pat_complete C SS (mset3 q)" by auto 
    from 1(1)[OF this] step show ?thesis by blast
  qed
qed

lemma simple_pat_complete_via_snd_step_NFs: "simple_pat_complete C SS (mset3 p) ⟷ 
  (∀ q. (p,q) ∈ ⇒⇩s⇩n⇩d⇧! ⟶ simple_pat_complete C SS (mset3 q))"
  using snd_steps_complete[of p] snd_steps(2)[of p] by blast

lemma snd_steps_NF_fvf_small_sort: assumes "finite_constructor_form_pat (mset3 p)" 
  and "(p,q) ∈ ⇒⇩s⇩n⇩d⇧!" 
shows "∀ mp ∈# q. ∀ eqc ∈# mp. ∀ t ∈# eqc. ∃ x ι. t = Var (x,ι) ∧ card_of_sort C ι ≤ size p"
proof -
  from snd_steps[of p q] assms 
  have fin: "finite_constructor_form_pat (mset3 q)" and 
    size: "size p ≥ size q" by blast+
  from assms have "q ∈ NF (⇒⇩s⇩n⇩d)" by auto
  hence "¬ (∃ Q. q ⇒⇩s⇩s Q ∧ Q ≠ {#})" using snd_step[OF _ fin] by blast
  from NF_spp_step_fvf_with_small_card[OF fin this] size show ?thesis by fastforce
qed

text ‹Major soundness properties of non-deterministic algorithm to transform FCF into FVF›
lemmas snd_step_combined = 
  snd_steps_bound ― ‹complexity›
  SN_snd_step     ― ‹termination›
  snd_steps_NF_fvf_small_sort ― ‹normal forms are in finite variable form with small sorts›
  simple_pat_complete_via_snd_step_NFs ― ‹equivalence: complete iff all normal forms are complete›

(* ************************************* 
     algorithm with don't-care non-determinism, 
     i.e., which can be implemented deterministically;
     this algorithm allows to invoke decision procedure for problems in finite variable form
   ************************************* *)

inductive_set spp_det_step_ms :: "('f,'s)simple_pat_problem_ms multiset rel" (‹⇛⇩s⇩s›)
  where spp_non_det_step: "p ⇒⇩s⇩s P' ⟹ finite_constructor_form_pat (mset3 p) ⟹ (add_mset p P, P' + P) ∈ ⇛⇩s⇩s" 
  | spp_non_det_fail: "P ≠ {#} ⟹ (add_mset {#} P, {#{#}#}) ∈ ⇛⇩s⇩s" 
  (* for finite-variable-form, we allow to just decide solvability *)
  | spp_fvf_succ: "(⋀ t. t ∈# ∑⇩# (image_mset ∑⇩# p) ⟹ is_Var t) ⟹ simple_pat_complete C SS (mset3 p)
      ⟹ (add_mset p P, P) ∈ ⇛⇩s⇩s" 
  | spp_fvf_fail: "(⋀ t. t ∈# ∑⇩# (image_mset ∑⇩# p) ⟹ is_Var t) ⟹ ¬ simple_pat_complete C SS (mset3 p)
      ⟹ finite_constructor_form_pat (mset3 p) ⟹ p ≠ {#} ⟹ (add_mset p P, {#{#}#}) ∈ ⇛⇩s⇩s" 
  
definition spp_det_prob :: "('f,'s)simple_pat_problem_ms multiset ⇒ bool" where
  "spp_det_prob P = (∀ p ∈# P. finite_constructor_form_pat (mset3 p))" 

definition spp_pat_complete :: "('f,'s)simple_pat_problem_ms multiset ⇒ bool" where
  "spp_pat_complete P = (∀ p ∈# P. simple_pat_complete C SS (mset3 p))" 

lemma spp_det_prob_add[simp]: "spp_det_prob (add_mset p P) = 
  (finite_constructor_form_pat (mset3 p) ∧ spp_det_prob P)" 
  unfolding spp_det_prob_def by simp

lemma spp_det_prob_plus[simp]: "spp_det_prob (P + P') = 
  (spp_det_prob P ∧ spp_det_prob P')" 
  unfolding spp_det_prob_def by auto

lemma spp_det_prob_empty[simp]: "spp_det_prob {#}" 
  by (simp add: spp_det_prob_def)

lemma spp_det_step_ms: "(P,P') ∈ ⇛⇩s⇩s ⟹ 
  spp_pat_complete P = spp_pat_complete P' ∧ (spp_det_prob P ⟶ spp_det_prob P')"
proof (induct rule: spp_det_step_ms.induct)
  case *: (spp_non_det_step p P' P)
  from spp_step_ms[OF *(1), folded spp_det_prob_def] *(2)
  show ?case by (auto simp: spp_pat_complete_def)
next
  case *: (spp_non_det_fail P)
  show ?case using detect_unsat_spp by (simp add: finite_constructor_form_pat_def spp_pat_complete_def)
next
  case (spp_fvf_succ p P)
  thus ?case by (auto simp: spp_pat_complete_def)
next
  case (spp_fvf_fail p P)
  thus ?case using detect_unsat_spp by (simp add: finite_constructor_form_pat_def spp_pat_complete_def)
qed

lemma spp_det_steps_ms: "(P,P') ∈ ⇛⇩s⇩s⇧* ⟹ 
  spp_pat_complete P = spp_pat_complete P' ∧ (spp_det_prob P ⟶ spp_det_prob P')"
  by (induct rule: rtrancl_induct, insert spp_det_step_ms, auto)

lemma SN_spp_det_step: "SN ⇛⇩s⇩s" 
proof (rule SN_subset)
  show "⇛⇩s⇩s ⊆ (mult (measure measure_p))^-1" 
  proof (standard, simp, goal_cases)
    case (1 P P')
    thus ?case
    proof (induct rule: spp_det_step_ms.induct)
      case *: (spp_non_det_step p P' P)
      from spp_step_complexity_and_termination[OF *(1-2)] show ?case
        by (simp add: add_many_mult)
    next
      case *: (spp_non_det_fail P)
      then obtain p P' where P: "P = add_mset p P'" by (cases P, auto)
      show ?case unfolding P by (simp add: subset_implies_mult)
    next
      case (spp_fvf_succ p P)
      show ?case by (simp add: subset_implies_mult)
    next
      case *: (spp_fvf_fail p P)      
      then obtain mp p' where p: "p = add_mset mp p'" by (cases p, auto)
      with *(2) have "mp ≠ {#}" unfolding simple_pat_complete_def simple_match_complete_wrt_def by auto
      then obtain eq mp' where mp: "mp = add_mset eq mp'" by (cases mp, auto)
      with *(3,4) have eq: "eq ≠ {#}" 
        unfolding finite_constructor_form_pat_def finite_constructor_form_mp_def mp p
        by auto
      have p: "measure_p p > 0" unfolding measure_p_def p num_syms_p_def num_syms_smp_def mp 
        using eq by (cases eq, auto)
      have e: "measure_p {#} = 0" unfolding measure_p_def p num_syms_p_def max_depth_sort_p_def
        max_dupl_p_def by auto
      from p e have "({#}, p) ∈ measure measure_p" by auto
      thus ?case
        by (metis add_cancel_left_left add_mset_eq_single empty_not_add_mset multi_member_split
            one_step_implies_mult union_single_eq_member)
    qed
  qed
  show "SN ((mult (measure measure_p))¯)" 
    by (rule wf_imp_SN, simp add: wf_mult[OF wf_measure])
qed

lemma NF_spp_det_step: assumes "spp_det_prob P" 
  and "P ∈ NF ⇛⇩s⇩s" 
shows "P = {#} ∨ P = {#{#}#}"
proof (rule ccontr)
  assume contr: "¬ ?thesis" 
  from assms(2) have NF: "(P,P') ∈ ⇛⇩s⇩s ⟹ False" for P' by auto
  from contr obtain p P2 where P: "P = add_mset p P2" and disj: "p ≠ {#} ∨ P2 ≠ {#}" by (cases P, auto)
  from assms[unfolded P] have fin: "finite_constructor_form_pat (mset3 p)" by auto 
  show False
  proof (cases "p = {#}")
    case True
    with disj have P2: "P2 ≠ {#}" by auto
    show False 
      apply (rule NF)
      apply (unfold P True)
      by (rule spp_non_det_fail[OF P2])
  next
    case False
    have "∄P. p ⇒⇩s⇩s P ∧ P ≠ {#}" using NF[unfolded P, OF spp_non_det_step[OF _ fin]] by auto
    note fvf = normal_form_spp_step_fvf[OF fin this]
    show ?thesis
    proof (cases "simple_pat_complete C SS (mset3 p)")
      case True
      show False
        by (rule NF, unfold P, rule spp_fvf_succ[OF _ True], insert fvf, auto)
    next
      case unsat: False
      show False
        by (rule NF, unfold P, rule spp_fvf_fail[OF _ unsat fin False], insert fvf, auto)
    qed
  qed
qed

lemma decision_procedure_spp_det:
  assumes  valid_input: "spp_det_prob P" and NF: "(P,Q) ∈ ⇛⇩s⇩s⇧!"
  shows "Q = {#} ∧ spp_pat_complete P ― ‹either the result is {} and input P is complete›
  ∨ Q = {#{#}#} ∧ ¬ spp_pat_complete P ― ‹or the result = bot and P is not complete›" 
proof -
  from NF have steps: "(P,Q) ∈ ⇛⇩s⇩s⇧*" and Q: "Q ∈ NF ⇛⇩s⇩s" by auto
  from spp_det_steps_ms[OF steps] valid_input
  have equiv: "spp_pat_complete P = spp_pat_complete Q" and valid_out: "spp_det_prob Q" by auto
  from NF_spp_det_step[OF valid_out Q]
  show ?thesis
  proof
    assume "Q = {#}" 
    thus ?thesis unfolding equiv by (simp add: spp_pat_complete_def)
  next
    assume "Q = {#{#}#}"
    thus ?thesis unfolding equiv using detect_unsat_spp by (simp add: spp_pat_complete_def)
  qed
qed 
    
text ‹A combined complexity approximation›

text ‹Conversion from pattern problems in finite constructor form to their simplified representation,
  performed on multiset-representation›
definition fcf_mp_to_smp :: "('f,'v,'s)match_problem_mset ⇒ ('f,'s)simple_match_problem_ms" where
  "fcf_mp_to_smp mp = (let xs = mset_set ((the_Var o snd) ` set_mset mp)
     in image_mset (λ x. image_mset fst (filter_mset (λ (t,l). l = Var x) mp)) xs)" 

lemma fcf_mp_to_smp: assumes fcf: "finite_constr_form_mp C (set_mset mp)" 
  and no_fail: "¬ match_fail mp" 
  and wf_match: "wf_match (set_mset mp)" 
  shows "finite_constructor_form_mp (mset2 (fcf_mp_to_smp mp))" 
  unfolding finite_constructor_form_mp_def
proof
  fix seqc
  assume "seqc ∈ mset2 (fcf_mp_to_smp mp)" 
  from this[unfolded fcf_mp_to_smp_def Let_def, simplified]
  obtain x tx eqc where tx: "tx ∈# mp" and x: "x = the_Var (snd tx)"  
    and eqc: "eqc = image_mset fst {#(t, l) ∈# mp. l = Var x#}" 
    and seqc: "seqc = set_mset eqc" by force
  from fcf[unfolded finite_constr_form_mp_def, rule_format, of "fst tx" "snd tx"] tx x
  obtain t ι where tx: "(t,Var x) ∈# mp" and fin: "finite_sort C ι" and t: "t : ι in 𝒯(C,𝒱)" 
    by (cases tx, auto)
  from tx eqc seqc have seqc1: "seqc ≠ {}" by auto
  {
    fix t'
    assume "t' ∈ seqc" 
    from this[unfolded seqc eqc] have t': "(t',Var x) ∈# mp" by auto
    have "𝒯(C,𝒱) t' = 𝒯(C,𝒱) t" 
    proof (rule ccontr)
      let ?p1 = "(t,Var x)" 
      let ?p2 = "(t',Var x)" 
      define mp' where "mp' = mp - {# ?p1, ?p2 #}" 
      assume "¬ ?thesis" 
      hence "?p1 ≠ ?p2" by auto
      with tx t' have "mp = add_mset ?p1 (add_mset ?p2 mp')" 
        unfolding mp'_def using multi_member_split by fastforce
      from match_clash_sort[of t t' x mp', folded this] ‹¬ ?thesis› no_fail
      show False by auto
    qed
    with t have t'i: "t' : ι in 𝒯(C,𝒱)" unfolding hastype_def by auto
    from wf_match[unfolded wf_match_def tvars_match_def] t' have "vars t' ⊆ SS" by force
    with t'i have "t' : ι in 𝒯(C,𝒱 |` SS)" 
      by (meson hastype_in_Term_mono_right hastype_in_Term_restrict_vars restrict_map_mono_right)
  }
  with fin seqc1
  show "seqc ≠ {} ∧ (∃ι. finite_sort C ι ∧ (∀t∈seqc. t : ι in 𝒯(C,𝒱 |` SS)))" 
    by auto
qed

definition fcf_pat_to_spat :: "('f,'v,'s)pat_problem_mset ⇒ ('f,'s)simple_pat_problem_ms" where
  "fcf_pat_to_spat = image_mset fcf_mp_to_smp" 

lemma fcf_pat_to_spat: assumes fcf: "finite_constr_form_pat C (pat_mset p)" 
  and NF: "p ∈ NF ( ⇒⇩n⇩d )" 
  and wf_pat: "wf_pat (pat_mset p)" 
shows "finite_constructor_form_pat (mset3 (fcf_pat_to_spat p))" 
  unfolding finite_constructor_form_pat_def
proof
  fix ssmp
  assume "ssmp ∈ mset3 (fcf_pat_to_spat p)" 
  then obtain smp where "smp ∈# fcf_pat_to_spat p" and ssmp: "ssmp = mset2 smp" by auto
  from this[unfolded fcf_pat_to_spat_def] obtain mp where mp: "mp ∈# p" and 
    smp: "smp = fcf_mp_to_smp mp" by auto
  with ssmp have ssmp: "ssmp = mset2 (fcf_mp_to_smp mp)" by auto
  show "finite_constructor_form_mp ssmp" unfolding ssmp
  proof (rule fcf_mp_to_smp)
    from fcf[unfolded finite_constr_form_pat_def] mp
    show "finite_constr_form_mp C (mp_mset mp)" by auto
    from wf_pat[unfolded wf_pat_def] mp 
    show "wf_match (mp_mset mp)" by auto
    show "¬ match_fail mp" 
    proof
      from mp obtain p' where p: "p = add_mset mp p'" by (metis mset_add)
      assume "match_fail mp" 
      from pat_remove_mp[OF this, of p', folded p]
      have "p ⇒⇩m {#p'#}" .
      hence "(p,p') ∈ ⇒⇩n⇩d" by (intro pp_nd_step_mset.intros, auto)
      with NF show False by auto
    qed
  qed
qed

lemma wf_pat_nd_step: "(p,q) ∈ ⇒⇩n⇩d ⟹ wf_pat (pat_mset p) ⟹ wf_pat (pat_mset q)" 
  by (smt (verit, ccfv_SIG) comp_def image_iff p_step_mset_imp_set pp_nd_step_mset.cases
      pp_step_wf)

lemma sum_smp_fcf_mp_to_smp_is_image_fst: 
  assumes "finite_constr_form_mp C (mp_mset mp)"
  shows "sum_mset (fcf_mp_to_smp mp) = image_mset fst mp"
  using assms
proof (induct "size mp" arbitrary: mp rule: less_induct)
  case (less mp)
  show ?case
  proof (cases mp)
    case empty
    thus ?thesis by (auto simp: fcf_mp_to_smp_def)
  next
    case (add tx mp')
    from less(2)[unfolded finite_constr_form_mp_def add]
    obtain t x where tx: "tx = (t,Var x)" by (cases tx; cases "snd tx"; auto)
    define mp1 where "mp1 = filter_mset (λ ty. snd ty = Var x) mp" 
    from tx add have tx: "(t, Var x) ∈# mp1" by (auto simp: mp1_def)
    define mp2 where "mp2 = filter_mset (Not o (λ ty. snd ty = Var x)) mp" 
    define ys where "ys = mset_set {the_Var (snd y) |. y ∈ mp_mset mp2}" 
    from tx have x: "x ∈ {the_Var (snd x) |. x ∈ mp_mset mp1 ∪ mp_mset mp2}" by force
    from less(2) have fcf: "finite_constr_form_mp C (mp_mset mp2)" 
      unfolding finite_constr_form_mp_def mp2_def by auto
    have mp: "mp = mp1 + mp2" unfolding mp1_def mp2_def by auto
    have x2: "x ∉ ((the_Var ∘ snd) ` mp_mset mp2)" unfolding mp2_def 
      using less(2)[unfolded finite_constr_form_mp_def]
      by auto
    hence xys: "x ∉# ys" unfolding ys_def by auto
    have "(the_Var ∘ snd) ` mp_mset mp = 
        insert x (((the_Var ∘ snd) ` mp_mset mp2))" 
      using x unfolding mp by (auto simp: mp1_def)
    from arg_cong[OF this, of mset_set]
    have xs: "mset_set ((the_Var ∘ snd) ` mp_mset mp) = add_mset x (mset_set (((the_Var ∘ snd) ` mp_mset mp2)))" 
      using x2 by auto
    have "fcf_mp_to_smp mp = add_mset (image_mset fst mp1)
     {#image_mset fst {#(t, l) ∈# mp. l = Var y#}. y ∈# ys#}" 
      unfolding fcf_mp_to_smp_def xs Let_def ys_def
      by (auto simp add: mp1_def intro!: arg_cong[of _ _ "image_mset fst"]) (induct mp, auto)
    also have "{#image_mset fst {#(t, l) ∈# mp. l = Var y#}. y ∈# ys#} =
        {#image_mset fst {#(t, l) ∈# mp2. l = Var y#}. y ∈# ys#}" 
      unfolding mp using xys
    proof (induct ys)
      case (add y ys)
      hence "x ≠ y" by auto
      hence "{#(t, l) ∈# mp1. l = Var y#} = {#}" unfolding mp1_def by (induct mp, auto)
      with add show ?case by auto
    qed auto
    also have "… = fcf_mp_to_smp mp2" unfolding fcf_mp_to_smp_def Let_def ys_def by auto
    finally have "sum_mset (fcf_mp_to_smp mp) = 
       image_mset fst mp1 + sum_mset (fcf_mp_to_smp mp2)" 
      by (auto simp: num_syms_smp_def)
    also have "sum_mset (fcf_mp_to_smp mp2) = image_mset fst mp2" using less(1)[OF _ fcf]
      unfolding mp using tx by (cases mp1, auto)
    finally show ?thesis unfolding mp by auto
  qed
qed

lemma num_syms_smp_fcf_mp_to_smp_is_meas_tsymbols: 
  assumes "finite_constr_form_mp C (mp_mset mp)"
  shows "num_syms_smp (fcf_mp_to_smp mp) = num_tsyms_mp mp"
proof -
  let ?mp = "fcf_mp_to_smp mp" 
  have "num_syms_smp ?mp = (∑x∈#mp. num_syms (fst x))" 
    unfolding num_syms_smp_def sum_smp_fcf_mp_to_smp_is_image_fst[OF assms] image_mset.compositionality o_def
    by simp
  also have "… = num_tsyms_mp mp" 
    unfolding num_tsyms_mp_def o_def by simp
  finally show ?thesis .
qed


lemma num_syms_p_fcf_pat_to_spat_is_meas_tsymbols: 
  assumes "finite_constr_form_pat C (pat_mset p)"
  shows "num_syms_p (fcf_pat_to_spat p) = meas_tsymbols p" 
  using num_syms_smp_fcf_mp_to_smp_is_meas_tsymbols assms
  unfolding num_syms_p_def meas_tsymbols_def finite_constr_form_pat_def fcf_pat_to_spat_def
  unfolding image_mset.compositionality o_def
  by (metis image_eqI image_mset_cong)

lemma measure_pat_poly_to_measure_p:
  assumes "finite_constr_form_pat C (pat_mset p)"
    and "finite_constructor_form_pat (mset3 (fcf_pat_to_spat p))" 
    and c: "card (dom C) * size p ≤ c" 
  shows "measure_p (fcf_pat_to_spat p) ≤ measure_pat_poly c p" 
proof -
  show ?thesis 
    unfolding measure_p_def measure_pat_poly_def
    unfolding num_syms_p_fcf_pat_to_spat_is_meas_tsymbols[OF assms(1)]
  proof (intro add_mono le_refl mult_mono)  
    from max_depth_sort_p_le_card_size[OF assms(2)] c
    show "max_depth_sort_p (fcf_pat_to_spat p) ≤ c + meas_diff p" 
      unfolding fcf_pat_to_spat_def by simp
    have "max_dupl_p (fcf_pat_to_spat p) = meas_dupl p" 
      unfolding meas_dupl_def max_dupl_p_def fcf_pat_to_spat_def image_mset.compositionality o_def
    proof (intro arg_cong[of _ _ sum_mset] image_mset_cong)
      fix mp
      assume "mp ∈# p"
      with assms[unfolded finite_constr_form_pat_def] 
      have fcf: "finite_constr_form_mp C (mp_mset mp)" by auto
      have "⋃ (⋃ ((`) vars ` mset2 (fcf_mp_to_smp mp)))
        = ⋃ (vars ` (set_mset (∑⇩# (fcf_mp_to_smp mp))))" by auto
      also have "… = ⋃ (vars ` fst ` set_mset mp)" unfolding 
          sum_smp_fcf_mp_to_smp_is_image_fst[OF fcf] by auto
      also have "… = tvars_match (mp_mset mp)" 
        unfolding tvars_match_def o_def by auto
      finally have id1: "⋃ (⋃ ((`) vars ` mset2 (fcf_mp_to_smp mp))) = tvars_match (mp_mset mp)" .
      show "max_dupl_smp (fcf_mp_to_smp mp) = max_dupl_mp mp" 
        unfolding max_dupl_smp_def max_dupl_mp_def id1 
        unfolding image_mset.compositionality o_def
        unfolding sum_smp_fcf_mp_to_smp_is_image_fst[OF fcf]
      proof (intro arg_cong[of _ _ Max] arg_cong[of _ _ "insert 0"] image_cong refl) 
        fix x 
        show "(∑t∈#image_mset fst mp. count (syms_term t) (Inl x)) = (∑tl∈#mp. count (syms_term (fst tl)) (Inl x))" 
          by (induct mp, auto)
      qed
    qed
    thus "max_dupl_p (fcf_pat_to_spat p) ≤ meas_dupl p" by simp
  qed auto
qed


theorem complexity_combined: fixes p :: "('f,'v,'s)pat_problem_mset" 
  assumes impr: improved "infinite (UNIV :: 'v set)" 
    and wf: "wf_pat (pat_mset p)" 
    and phase1: "(p,p1) ∈ ⇒⇩n⇩d ^^ n1" "(p,p1) ∈ ⇒⇩n⇩d⇧!"  
    and translation: "p1' = fcf_pat_to_spat p1" 
    and phase2: "(p1',p2) ∈ ⇒⇩s⇩n⇩d ^^ n2" 
  shows "n1 + n2 + num_syms_p p2 ≤ (card (dom C) * size p + num_syms_pat p) * (num_syms_pat p * m + 2)" 
    "size p2 ≤ size p"
    "p2 ∈ NF ⇒⇩s⇩n⇩d ⟹ mp ∈# p2 ⟹ eqc ∈# mp ⟹ t ∈# eqc ⟹ (x,ι) ∈ vars t ⟹ card_of_sort C ι ≤ size p" 
proof -
  define c where "c = card (dom C) * size p"
  note nd = nd_step_improved[OF impr wf] 
  from nd(2)[OF phase1(1), of c] 
  have n1: "measure_pat_poly c p1 + n1 ≤ (c + num_syms_pat p) * (num_syms_pat p * m + 2)" .
  from phase1(2) have NF: "p1 ∈ NF (⇒⇩n⇩d)" by auto
  from phase1 have star: "(p,p1) ∈ ⇒⇩n⇩d⇧*" by auto
  from nd_steps_le_size[OF star] 
  have pp1: "size p1 ≤ size p" and c: "card (dom C) * size p1 ≤ c" unfolding c_def by auto
  from pp1 have p1'p: "size p1' ≤ size p" unfolding translation fcf_pat_to_spat_def by auto
  from nd(3)[OF phase1(2)] 
  have fcf: "finite_constr_form_pat C (pat_mset p1)" by auto
  from star wf have "wf_pat (pat_mset p1)" using wf_pat_nd_step by (rule rtrancl_induct)
  from fcf_pat_to_spat[OF fcf NF this, folded translation]
  have fcf': "finite_constructor_form_pat (mset3 p1')" .
  from measure_pat_poly_to_measure_p[OF fcf, folded translation, OF fcf' c] n1
  have "measure_p p1' + n1 ≤ (c + num_syms_pat p) * (num_syms_pat p * m + 2)" 
    by auto
  with snd_bound_steps[OF phase2(1)]
  have "measure_p p2 + n2 + n1 ≤ (c + num_syms_pat p) * (num_syms_pat p * m + 2)" by auto
  moreover have "num_syms_p p2 ≤ measure_p p2" unfolding measure_p_def by auto
  ultimately show "n1 + n2 + num_syms_p p2 ≤ (c + num_syms_pat p) * (num_syms_pat p * m + 2)" by auto
  from phase2 have "(p1',p2) ∈ ⇒⇩s⇩n⇩d⇧*" by (rule relpow_imp_rtrancl)
  with fcf' have "size p2 ≤ size p1'" by (metis snd_steps(1))
  with p1'p show "size p2 ≤ size p" by simp
  
  assume NF: "p2 ∈ NF ⇒⇩s⇩n⇩d" and mp: "mp ∈# p2" and e: "eqc ∈# mp" and t: "t ∈# eqc" and x: "(x,ι) ∈ vars t" 
  from NF phase2 have "(p1',p2) ∈ ⇒⇩s⇩n⇩d⇧!"
    by (meson normalizability_I relpow_imp_rtrancl)
  from snd_steps_NF_fvf_small_sort[OF fcf' this, rule_format, OF mp e t] x
  have "card_of_sort C ι ≤ size p1'" by auto
  also have "… ≤ size p" by fact
  finally show "card_of_sort C ι ≤ size p" .
qed
end

end