Theory Typing_Result

(*  Title:      Typing_Result.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹The Typing Result›
text‹\label{sec:Typing-Result}›
theory Typing_Result
imports Typed_Model
begin

subsection ‹Locale Setup›
locale typing_result = typed_model arity public Ana Γ
  for arity::"'fun  nat"
    and public::"'fun  bool"
    and Ana::"('fun,'var) term  (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term  ('fun,'atom::finite) term_type"
  +
  assumes infinite_typed_consts: "a. infinite {c. Γ (Fun c []) = TAtom a  public c}"
    and no_private_funs[simp]: "f. arity f > 0  public f"
begin

subsubsection ‹Minor Lemmata›

lemma fun_type_inv': assumes "Γ t = TComp f T" shows "arity f > 0" "public f"
using assms fun_type_inv by simp_all

lemma infinite_public_consts[simp]: "infinite {c. public c  arity c = 0}"
proof -
  fix a::'atom
  define A where "A  {c. Γ (Fun c []) = TAtom a  public c}"
  define B where "B  {c. public c  arity c = 0}"

  have "arity c = 0" when c: "c  A" for c
    using c const_type_inv unfolding A_def by blast
  hence "A  B" unfolding A_def B_def by blast
  hence "infinite B"
    using infinite_typed_consts[of a, unfolded A_def[symmetric]]
    by (metis infinite_super)
  thus ?thesis unfolding B_def by blast
qed

lemma infinite_fun_syms[simp]:
  "infinite {c. public c  arity c > 0}  infinite Σf"
  "infinite 𝒞" "infinite 𝒞pub" "infinite (UNIV::'fun set)"
by (metis Σf_unfold finite_Collect_conjI,
    metis infinite_public_consts finite_Collect_conjI,
    use infinite_public_consts 𝒞pub_unfold in force simp add: Collect_conj_eq,
    metis UNIV_I finite_subset subsetI infinite_public_consts(1))

lemma id_univ_proper_subset[simp]: "Σf  UNIV" "(f. arity f > 0)  𝒞  UNIV"
by (metis finite.emptyI inf_top.right_neutral top.not_eq_extremum disjoint_fun_syms
          infinite_fun_syms(2) inf_commute)
   (metis top.not_eq_extremum UNIV_I const_arity_eq_zero less_irrefl)

lemma exists_fun_notin_funs_term: "f::'fun. f  funs_term t"
by (metis UNIV_eq_I finite_fun_symbols infinite_fun_syms(4))

lemma exists_fun_notin_funs_terms:
  assumes "finite M" shows "f::'fun. f  (funs_term ` M)"
by (metis assms finite_fun_symbols infinite_fun_syms(4) ex_new_if_finite finite_UN)

lemma exists_notin_funsst: "f. f  funsst (S::('fun,'var) strand)"
by (metis UNIV_eq_I finite_funsst infinite_fun_syms(4))

lemma infinite_typed_consts': "infinite {c. Γ (Fun c []) = TAtom a  public c  arity c = 0}"
proof -
  { fix c assume "Γ (Fun c []) = TAtom a" "public c"
    hence "arity c = 0" using const_type[of c] fun_type[of c "[]"] by auto
  } hence "{c. Γ (Fun c []) = TAtom a  public c  arity c = 0} =
           {c. Γ (Fun c []) = TAtom a  public c}"
    by auto
  thus "infinite {c. Γ (Fun c []) = TAtom a  public c  arity c = 0}"
    using infinite_typed_consts[of a] by metis
qed

lemma atypes_inhabited: "c. Γ (Fun c []) = TAtom a  wftrm (Fun c [])  public c  arity c = 0"
proof -
  obtain c where "Γ (Fun c []) = TAtom a" "public c" "arity c = 0"
    using infinite_typed_consts'(1)[of a] not_finite_existsD by blast
  thus ?thesis using const_type_inv[OF Γ (Fun c []) = TAtom a] unfolding wftrm_def by auto
qed

lemma atype_ground_term_ex: "t. fv t = {}  Γ t = TAtom a  wftrm t"
using atypes_inhabited[of a] by force

lemma type_ground_inhabited: "t'. fv t' = {}  Γ t = Γ t'"
proof -
  { fix τ::"('fun, 'atom) term_type" assume "f T. Fun f T  τ  0 < arity f"
    hence "t'. fv t' = {}  τ = Γ t'"
    proof (induction τ)
      case (Fun f T)
      hence "arity f > 0" by auto
    
      from Fun.IH Fun.prems(1) have "Y. map Γ Y = T  (x  set Y. fv x = {})"
      proof (induction T)
        case (Cons x X)
        hence "g Y. Fun g Y  Fun f X  0 < arity g" by auto
        hence "Y. map Γ Y = X  (xset Y. fv x = {})" using Cons by auto
        moreover have "t'. fv t' = {}  x = Γ t'" using Cons by auto
        ultimately obtain y Y where
            "fv y = {}" "Γ y = x" "map Γ Y = X" "xset Y. fv x = {}" 
          using Cons by atomize_elim auto
        hence "map Γ (y#Y) = x#X  (xset (y#Y). fv x = {})" by auto
        thus ?case by meson 
      qed simp
      then obtain Y where "map Γ Y = T" "x  set Y. fv x = {}" by metis
      hence "fv (Fun f Y) = {}" "Γ (Fun f Y) = TComp f T" using fun_type[OF arity f > 0] by auto
      thus ?case by (metis exI[of "λt. fv t = {}  Γ t = TComp f T" "Fun f Y"])
    qed (metis atype_ground_term_ex)
  }
  thus ?thesis by (metis Γ_wf'')
qed

lemma type_wfttype_inhabited:
  assumes "f T. Fun f T  τ  0 < arity f" "wftrm τ"
  shows "t. Γ t = τ  wftrm t"
using assms
proof (induction τ)
  case (Fun f Y)
  have IH: "t. Γ t = y  wftrm t" when y: "y  set Y " for y
  proof -
    have "wftrm y"
      using Fun y unfolding wftrm_def
      by (metis Fun_param_is_subterm term.le_less_trans) 
    moreover have "Fun g Z  y  0 < arity g" for g Z
      using Fun y by auto
    ultimately show ?thesis using Fun.IH[OF y] by auto
  qed

  from Fun have "arity f = length Y" "arity f > 0" unfolding wftrm_def by force+
  moreover from IH have "X. map Γ X = Y  (x  set X. wftrm x)"
    by (induct Y, simp_all, metis list.simps(9) set_ConsD)
  ultimately show ?case by (metis fun_type length_map wf_trmI)
qed (use atypes_inhabited wftrm_def in blast)

lemma type_pgwt_inhabited: "wftrm t  t'. Γ t = Γ t'  public_ground_wf_term t'"
proof -
  assume "wftrm t"
  { fix τ assume "Γ t = τ"
    hence "t'. Γ t = Γ t'  public_ground_wf_term t'" using wftrm t
    proof (induction τ arbitrary: t)
      case (Var a t)
      then obtain c where "Γ t = Γ (Fun c [])" "arity c = 0" "public c"
        using const_type_inv[of _ "[]" a] infinite_typed_consts(1)[of a]  not_finite_existsD
        by force
      thus ?case using PGWT[OF public c, of "[]"] by auto
    next
      case (Fun f Y t)
      have *: "arity f > 0" "public f" "arity f = length Y"
        using fun_type_inv[OF Γ t = TComp f Y] fun_type_inv_wf[OF Γ t = TComp f Y wftrm t]
        by auto
      have "y. y  set Y  t'. y = Γ t'  public_ground_wf_term t'"
        using Fun.prems(1) Fun.IH Γ_wf''[of _ _ t] Γ_wf'[OF wftrm t] type_wfttype_inhabited
        by (metis Fun_param_is_subterm term.order_trans wf_trm_subtermeq) 
      hence "X. map Γ X = Y  (x  set X. public_ground_wf_term x)"
        by (induct Y, simp_all, metis list.simps(9) set_ConsD)
      then obtain X where X: "map Γ X = Y" "x. x  set X  public_ground_wf_term x" by atomize_elim auto
      hence "arity f = length X" using *(3) by auto
      have "Γ t = Γ (Fun f X)" "public_ground_wf_term (Fun f X)"
        using fun_type[OF *(1), of X] Fun.prems(1) X(1) apply simp
        using PGWT[OF *(2) arity f = length X X(2)] by metis
      thus ?case by metis
    qed
  }
  thus ?thesis using wftrm t by auto
qed

end

subsection ‹The Typing Result for the Composition-Only Intruder›
context typing_result
begin

subsubsection ‹Well-typedness and Type-Flaw Resistance Preservation›
context
begin

private lemma LI_preserves_tfr_stp_all_single:
  assumes "(S,θ)  (S',θ')" "wfconstr S θ" "wtsubst θ"
  and "list_all tfrstp S" "tfrset (trmsst S)" "wftrms (trmsst S)"
  shows "list_all tfrstp S'"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' θ)
  hence "list_all tfrstp S" "list_all tfrstp S'" by simp_all
  moreover have "list_all tfrstp (map Send1 X)" by (induct X) auto
  ultimately show ?case by simp
next
  case (Unify S f Y δ X S' θ)
  hence "list_all tfrstp (S@S')" by simp

  have "fvst (S@Send1 (Fun f X)#S')  bvarsst (S@S') = {}"
    using Unify.prems(1) by (auto simp add: wfconstr_def)
  moreover have "fv (Fun f X)  fvst (S@Send1 (Fun f X)#S')" by auto
  moreover have "fv (Fun f Y)  fvst (S@Send1 (Fun f X)#S')"
    using Unify.hyps(2) fv_subset_if_in_strand_ik'[of "Fun f Y" S] by force
  ultimately have bvars_disj:
      "bvarsst (S@S')  fv (Fun f X) = {}" "bvarsst (S@S')  fv (Fun f Y) = {}"
    by blast+

  have "wftrm (Fun f X)" using Unify.prems(5) by simp
  moreover have "wftrm (Fun f Y)"
  proof -
    obtain x where "x  set S" "Fun f Y  subtermsset (trmsstp x)" "wftrms (trmsstp x)"
      using Unify.hyps(2) Unify.prems(5) by force+
    thus ?thesis using wf_trm_subterm by auto
  qed
  moreover have
      "Fun f X  SMP (trmsst (S@Send1 (Fun f X)#S'))"
      "Fun f Y  SMP (trmsst (S@Send1 (Fun f X)#S'))"
    using SMP_append[of S "Send1 (Fun f X)#S'"] SMP_Cons[of "Send1 (Fun f X)" S']
          SMP_ikI[OF Unify.hyps(2)]
    by auto
  hence "Γ (Fun f X) = Γ (Fun f Y)"
    using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
    unfolding tfrset_def by blast
  ultimately have "wtsubst δ" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Unify.hyps(3)[symmetric] wftrm (Fun f X) wftrm (Fun f Y)]
    by (metis wf_trm_subst_range_iff)
  moreover have "bvarsst (S@S')  range_vars δ = {}"
    using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] bvars_disj by fast
  ultimately show ?case using tfr_stp_all_wt_subst_apply[OF list_all tfrstp (S@S')] by metis
next
  case (Equality S δ t t' a S' θ)
  have "list_all tfrstp (S@S')" "Γ t = Γ t'"
    using tfr_stp_all_same_type[of S a t t' S']
          tfr_stp_all_split(5)[of S _ S']
          MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
          Equality.prems(3)
    by blast+
  moreover have "wftrm t" "wftrm t'" using Equality.prems(5) by auto
  ultimately have "wtsubst δ"
    using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]]
    by metis
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Equality.hyps(2)[symmetric] wftrm t wftrm t']
    by (metis wf_trm_subst_range_iff)
  moreover have "fvst (S@Equality a t t'#S')  bvarsst (S@Equality a t t'#S') = {}"
    using Equality.prems(1) by (auto simp add: wfconstr_def)
  hence "bvarsst (S@S')  fv t = {}" "bvarsst (S@S')  fv t' = {}" by auto
  hence "bvarsst (S@S')  range_vars δ = {}"
    using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by fast
  ultimately show ?case using tfr_stp_all_wt_subst_apply[OF list_all tfrstp (S@S')] by metis
qed

private lemma LI_in_SMP_subset_single:
  assumes "(S,θ)  (S',θ')" "wfconstr S θ" "wtsubst θ"
          "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  and "trmsst S  SMP M"
  shows "trmsst S'  SMP M"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' θ)
  hence "SMP (trmsst [Send1 (Fun f X)])  SMP M"
  proof -
    have "SMP (trmsst [Send1 (Fun f X)])  SMP (trmsst (S@Send1 (Fun f X)#S'))"
      using trmsst_append SMP_mono by auto
    thus ?thesis
      using SMP_union[of "trmsst (S@Send1 (Fun f X)#S')" M]
            SMP_subset_union_eq[OF Compose.prems(6)]
      by auto
  qed
  thus ?case using Compose.prems(6) by auto
next
  case (Unify S f Y δ X S' θ)
  have "Fun f X  SMP (trmsst (S@Send1 (Fun f X)#S'))" by auto
  moreover have "MGU δ (Fun f X) (Fun f Y)"
    by (metis mgu_gives_MGU[OF Unify.hyps(3)[symmetric]])
  moreover have
        "x. x  set S  wftrms (trmsstp x)" "wftrm (Fun f X)"
    using Unify.prems(4) by force+
  moreover have "Fun f Y  SMP (trmsst (S@Send1 (Fun f X)#S'))"
    by (meson SMP_ikI Unify.hyps(2) contra_subsetD ik_append_subset(1))
  ultimately have "wftrm (Fun f Y)" "Γ (Fun f X) = Γ (Fun f Y)"
    using ikst_subterm_exD[OF Fun f Y  ikst S] tfrset (trmsst (S@Send1 (Fun f X)#S'))
    unfolding tfrset_def by (metis (full_types) SMP_wf_trm Unify.prems(4), blast)
  hence "wtsubst δ" by (metis mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric] wftrm (Fun f X)])
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Unify.hyps(3)[symmetric] wftrm (Fun f X) wftrm (Fun f Y)] by simp
  ultimately have "trmsst ((S@Send1 (Fun f X)#S') st δ)  SMP M"
    using SMP.Substitution Unify.prems(6) wt_subst_SMP_subset by metis
  thus ?case by auto
next
  case (Equality S δ t t' a S' θ)
  hence "Γ t = Γ t'"
    using tfr_stp_all_same_type MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
    by metis
  moreover have "t  SMP (trmsst (S@Equality a t t'#S'))" "t'  SMP (trmsst (S@Equality a t t'#S'))"
    using Equality.prems(1) by auto
  moreover have "MGU δ t t'" using mgu_gives_MGU[OF Equality.hyps(2)[symmetric]] by metis
  moreover have "x. x  set S  wftrms (trmsstp x)" "wftrm t" "wftrm t'"
    using Equality.prems(4) by force+
  ultimately have "wtsubst δ" by (metis mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric] wftrm t])
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Equality.hyps(2)[symmetric] wftrm t wftrm t'] by simp
  ultimately have "trmsst ((S@Equality a t t'#S') st δ)  SMP M"
    using SMP.Substitution Equality.prems wt_subst_SMP_subset by metis
  thus ?case by auto
qed

private lemma LI_preserves_tfr_single:
  assumes "(S,θ)  (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
          "tfrset (trmsst S)" "wftrms (trmsst S)"
          "list_all tfrstp S"
  shows "tfrset (trmsst S')  wftrms (trmsst S')"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' θ)
  let ?SMPmap = "SMP (trmsst (S@map Send1 X@S')) - (Var`𝒱)"
  have "?SMPmap  SMP (trmsst (S@Send1 (Fun f X)#S')) - (Var`𝒱)"
    using SMP_fun_map_snd_subset[of X f]
          SMP_append[of "map Send1 X" S'] SMP_Cons[of "Send1 (Fun f X)" S']
          SMP_append[of S "Send1 (Fun f X)#S'"] SMP_append[of S "map Send1 X@S'"]
    by auto
  hence "s  ?SMPmap. t  ?SMPmap. (δ. Unifier δ s t)  Γ s = Γ t"
    using Compose unfolding tfrset_def by (meson subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Compose[OF Compose.hyps]], of S']
          Compose.prems(5)
    unfolding tfrset_def by blast
next
  case (Unify S f Y δ X S' θ)
  let ?SMPδ = "SMP (trmsst (S@S' st δ)) - (Var`𝒱)"

  have "SMP (trmsst (S@S' st δ))  SMP (trmsst (S@Send1 (Fun f X)#S'))"
  proof
    fix s assume "s  SMP (trmsst (S@S' st δ))" thus "s  SMP (trmsst (S@Send1 (Fun f X)#S'))"
      using LI_in_SMP_subset_single[
              OF LI_rel.Unify[OF Unify.hyps] Unify.prems(1,2,4,5,6)
                 MP_subset_SMP(2)[of "S@Send1 (Fun f X)#S'"]]
      by (metis SMP_union SMP_subset_union_eq Un_iff)
  qed
  hence "s  ?SMPδ. t  ?SMPδ. (δ. Unifier δ s t)  Γ s = Γ t"
    using Unify.prems(4) unfolding tfrset_def by (meson Diff_iff subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Unify[OF Unify.hyps]], of S']
          Unify.prems(5)
    unfolding tfrset_def by blast
next
  case (Equality S δ t t' a S' θ)
  let ?SMPδ = "SMP (trmsst (S@S' st δ)) - (Var`𝒱)"

  have "SMP (trmsst (S@S' st δ))  SMP (trmsst (S@Equality a t t'#S'))"
  proof
    fix s assume "s  SMP (trmsst (S@S' st δ))" thus "s  SMP (trmsst (S@Equality a t t'#S'))"
      using LI_in_SMP_subset_single[
              OF LI_rel.Equality[OF Equality.hyps] Equality.prems(1,2,4,5,6)
                 MP_subset_SMP(2)[of "S@Equality a t t'#S'"]]
      by (metis SMP_union SMP_subset_union_eq Un_iff)
  qed
  hence "s  ?SMPδ. t  ?SMPδ. (δ. Unifier δ s t)  Γ s = Γ t"
    using Equality.prems unfolding tfrset_def by (meson Diff_iff subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Equality[OF Equality.hyps]], of _ S']
          Equality.prems
    unfolding tfrset_def by blast
qed

private lemma LI_preserves_welltypedness_single:
  assumes "(S,θ)  (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
  and "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  shows "wtsubst θ'  wftrms (subst_range θ')"
using assms
proof (induction rule: LI_rel.induct)
  case (Unify S f Y δ X S' θ)
  have "wftrm (Fun f X)" using Unify.prems(5) unfolding tfrset_def by simp
  moreover have "wftrm (Fun f Y)"
  proof -
    obtain x where "x  set S" "Fun f Y  subtermsset (trmsstp x)" "wftrms (trmsstp x)"
      using Unify.hyps(2) Unify.prems(5) unfolding tfrset_def by force
    thus ?thesis using wf_trm_subterm by auto
  qed
  moreover have
      "Fun f X  SMP (trmsst (S@Send1 (Fun f X)#S'))" "Fun f Y  SMP (trmsst (S@Send1 (Fun f X)#S'))"
    using SMP_append[of S "Send1 (Fun f X)#S'"] SMP_Cons[of "Send1 (Fun f X)" S']
          SMP_ikI[OF Unify.hyps(2)]
    by auto
  hence "Γ (Fun f X) = Γ (Fun f Y)"
    using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
    unfolding tfrset_def by blast
  ultimately have "wtsubst δ" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis

  have "wftrms (subst_range δ)"
    by (meson mgu_wf_trm[OF Unify.hyps(3)[symmetric] wftrm (Fun f X) wftrm (Fun f Y)]
              wf_trm_subst_range_iff)
  hence "wftrms (subst_range (θ s δ))"
    using wf_trm_subst_range_iff wf_trm_subst wftrms (subst_range θ)
    unfolding subst_compose_def
    by (metis (no_types, lifting))
  thus ?case by (metis wt_subst_compose[OF wtsubst θ wtsubst δ])
next
  case (Equality S δ t t' a S' θ)
  have "wftrm t" "wftrm t'" using Equality.prems(5) by simp_all
  moreover have "Γ t = Γ t'"
    using list_all tfrstp (S@Equality a t t'#S')
          MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
    by auto
  ultimately have "wtsubst δ" using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]] by metis

  have "wftrms (subst_range δ)"
    by (meson mgu_wf_trm[OF Equality.hyps(2)[symmetric] wftrm t wftrm t'] wf_trm_subst_range_iff)
  hence "wftrms (subst_range (θ s δ))"
    using wf_trm_subst_range_iff wf_trm_subst wftrms (subst_range θ)
    unfolding subst_compose_def
    by (metis (no_types, lifting))
  thus ?case by (metis wt_subst_compose[OF wtsubst θ wtsubst δ])
qed metis

lemma LI_preserves_welltypedness:
  assumes "(S,θ) * (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
    and "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  shows "wtsubst θ'" (is "?A θ'")
    and "wftrms (subst_range θ')" (is "?B θ'")
proof -
  have "?A θ'  ?B θ'" using assms
  proof (induction S θ rule: converse_rtrancl_induct2)
    case (step S1 θ1 S2 θ2)
    hence "?A θ2  ?B θ2" using LI_preserves_welltypedness_single by presburger
    moreover have "wfconstr S2 θ2"
      by (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)])
    moreover have "tfrset (trmsst S2)" "wftrms (trmsst S2)"
      using LI_preserves_tfr_single[OF step.hyps(1)] step.prems by presburger+
    moreover have "list_all tfrstp S2"
      using LI_preserves_tfr_stp_all_single[OF step.hyps(1)] step.prems by fastforce
    ultimately show ?case using step.IH by presburger
  qed simp
  thus "?A θ'" "?B θ'" by simp_all
qed

lemma LI_preserves_tfr:
  assumes "(S,θ) * (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
    and "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  shows "tfrset (trmsst S')" (is "?A S'")
    and "wftrms (trmsst S')" (is "?B S'")
    and "list_all tfrstp S'" (is "?C S'")
proof -
  have "?A S'  ?B S'  ?C S'" using assms
  proof (induction S θ rule: converse_rtrancl_induct2)
    case (step S1 θ1 S2 θ2)
    have "wfconstr S2 θ2" "tfrset (trmsst S2)" "wftrms (trmsst S2)" "list_all tfrstp S2"
      using LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)]
            LI_preserves_tfr_single[OF step.hyps(1) step.prems(1,2)]
            LI_preserves_tfr_stp_all_single[OF step.hyps(1) step.prems(1,2)]
            step.prems(3,4,5,6)
      by metis+
    moreover have "wtsubst θ2" "wftrms (subst_range θ2)"
      using LI_preserves_welltypedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems]
      by simp_all
    ultimately show ?case using step.IH by presburger
  qed blast
  thus "?A S'" "?B S'" "?C S'" by simp_all
qed

lemma LI_preproc_preserves_tfr:
  assumes "tfrst S"
  shows "tfrst (LI_preproc S)"
unfolding tfrst_def
proof
  have S: "tfrset (trmsst S)" "list_all tfrstp S" using assms unfolding tfrst_def by metis+

  show "tfrset (trmsst (LI_preproc S))" by (metis S(1) LI_preproc_trms_eq)

  show "list_all tfrstp (LI_preproc S)" using S(2)
  proof (induction S)
    case (Cons x S)
    have IH: "list_all tfrstp (LI_preproc S)" using Cons by simp
    have x: "tfrstp x" using Cons.prems by simp

    show ?case using x IH unfolding list_all_iff by (cases x) auto
  qed simp
qed
end

subsubsection ‹Simple Constraints are Well-typed Satisfiable›
text ‹Proving the existence of a well-typed interpretation›
context
begin

lemma wt_interpretation_exists: 
  obtains ::"('fun,'var) subst"
  where "interpretationsubst " "wtsubst " "subst_range   public_ground_wf_terms"
proof
  define  where " = (λx. (SOME t. Γ (Var x) = Γ t  public_ground_wf_term t))"

  { fix x t assume " x = t"
    hence "Γ (Var x) = Γ t  public_ground_wf_term t"
      using someI_ex[of "λt. Γ (Var x) = Γ t  public_ground_wf_term t",
                     OF type_pgwt_inhabited[of "Var x"]]
      unfolding ℐ_def wftrm_def by simp
  } hence props: " v = t  Γ (Var v) = Γ t  public_ground_wf_term t" for v t by metis

  have " v  Var v" for v using props pgwt_ground by fastforce
  hence "subst_domain  = UNIV" by auto
  moreover have "ground (subst_range )" by (simp add: props pgwt_ground)
  ultimately show "interpretationsubst " by metis
  show "wtsubst " unfolding wtsubst_def using props by simp
  show "subst_range   public_ground_wf_terms" by (auto simp add: props)
qed

lemma wt_grounding_subst_exists:
  "θ. wtsubst θ  wftrms (subst_range θ)  fv (t  θ) = {}"
proof -
  obtain θ where θ: "interpretationsubst θ" "wtsubst θ" "subst_range θ  public_ground_wf_terms"
    using wt_interpretation_exists by blast
  show ?thesis using pgwt_wellformed interpretation_grounds[OF θ(1)] θ(2,3) by blast
qed

private fun fresh_pgwt::"'fun set  ('fun,'atom) term_type  ('fun,'var) term"  where
  "fresh_pgwt S (TAtom a) =
    Fun (SOME c. c  S  Γ (Fun c []) = TAtom a  public c) []"
| "fresh_pgwt S (TComp f T) = Fun f (map (fresh_pgwt S) T)"

private lemma fresh_pgwt_same_type:
  assumes "finite S" "wftrm t"
  shows "Γ (fresh_pgwt S (Γ t)) = Γ t"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ  (f T. TComp f T  τ  0 < arity f)"
  { fix τ assume "?P τ" hence "Γ (fresh_pgwt S τ) = τ"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c  S  Γ (Fun c []) = Var a  public c"
      let ?Q = "λc. Γ (Fun c []) = Var a  public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "c. ?P c" using not_finite_existsD by blast
      thus ?case using someI_ex[of ?P] by auto
    next
      case (Fun f T)
      have f: "0 < arity f" using Fun.prems fun_type_inv by auto
      have "t. t  set T  ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "t. t  set T  Γ (fresh_pgwt S t) = t" using Fun.prems Fun.IH by auto
      hence "map Γ (map (fresh_pgwt S) T) = T"  by (induct T) auto
      thus ?case using fun_type[OF f] by simp
    qed
  } thus ?thesis using assms(1) Γ_wf'[OF assms(2)] Γ_wf'' by auto
qed

private lemma fresh_pgwt_empty_synth:
  assumes "finite S" "wftrm t"
  shows "{} c fresh_pgwt S (Γ t)"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ  (f T. TComp f T  τ  0 < arity f)"
  { fix τ assume "?P τ" hence "{} c fresh_pgwt S τ"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c  S  Γ (Fun c []) = Var a  public c"
      let ?Q = "λc. Γ (Fun c []) = Var a  public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "c. ?P c" using not_finite_existsD by blast
      thus ?case
        using someI_ex[of ?P] intruder_synth.ComposeC[of "[]" _ "{}"] const_type_inv
        by auto
    next
      case (Fun f T)
      have f: "0 < arity f" "length T = arity f" "public f" 
        using Fun.prems fun_type_inv unfolding wftrm_def by auto
      have "t. t  set T  ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "t. t  set T  {} c fresh_pgwt S t" using Fun.prems Fun.IH by auto
      moreover have "length (map (fresh_pgwt S) T) = arity f" using f(2) by auto
      ultimately show ?case using intruder_synth.ComposeC[of "map (fresh_pgwt S) T" f] f by auto
    qed
  } thus ?thesis using assms(1) Γ_wf'[OF assms(2)] Γ_wf'' by auto
qed

private lemma fresh_pgwt_has_fresh_const:
  assumes "finite S" "wftrm t"
  obtains c where "Fun c []  fresh_pgwt S (Γ t)" "c  S"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ  (f T. TComp f T  τ  0 < arity f)"
  { fix τ assume "?P τ" hence "c. Fun c []  fresh_pgwt S τ  c  S"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c  S  Γ (Fun c []) = Var a  public c"
      let ?Q = "λc. Γ (Fun c []) = Var a  public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "c. ?P c" using not_finite_existsD by blast
      thus ?case using someI_ex[of ?P] by auto
    next
      case (Fun f T)
      have f: "0 < arity f" "length T = arity f" "public f" "T  []"
        using Fun.prems fun_type_inv unfolding wftrm_def by auto
      obtain t' where t': "t'  set T" by (meson all_not_in_conv f(4) set_empty) 
      have "t. t  set T  ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "t. t  set T  c. Fun c []  fresh_pgwt S t  c  S"
        using Fun.prems Fun.IH by auto
      then obtain c where c: "Fun c []  fresh_pgwt S t'" "c  S" using t' by metis
      thus ?case using t' by auto
    qed
  } thus ?thesis using that assms Γ_wf'[OF assms(2)] Γ_wf'' by blast 
qed

private lemma fresh_pgwt_subterm_fresh:
  assumes "finite S" "wftrm t" "wftrm s" "funs_term s  S"
  shows "s  subterms (fresh_pgwt S (Γ t))"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ  (f T. TComp f T  τ  0 < arity f)"
  { fix τ assume "?P τ" hence "s  subterms (fresh_pgwt S τ)"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c  S  Γ (Fun c []) = Var a  public c"
      let ?Q = "λc. Γ (Fun c []) = Var a  public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "c. ?P c" using not_finite_existsD by blast
      thus ?case using someI_ex[of ?P] assms(4) by auto
    next
      case (Fun f T)
      have f: "0 < arity f" "length T = arity f" "public f" 
        using Fun.prems fun_type_inv unfolding wftrm_def by auto
      have "t. t  set T  ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "t. t  set T  s  subterms (fresh_pgwt S t)" using Fun.prems Fun.IH by auto
      moreover have "s  fresh_pgwt S (Fun f T)"
      proof -
        obtain c where c: "Fun c []  fresh_pgwt S (Fun f T)" "c  S"
          using fresh_pgwt_has_fresh_const[OF assms(1)] type_wfttype_inhabited Fun.prems
          by metis
        hence "¬Fun c []  s" using assms(4) subtermeq_imp_funs_term_subset by force
        thus ?thesis using c(1) by auto
      qed
      ultimately show ?case by auto
    qed
  } thus ?thesis using assms(1) Γ_wf'[OF assms(2)] Γ_wf'' by auto
qed

private lemma wt_fresh_pgwt_term_exists:
  assumes "finite T" "wftrm s" "wftrms T"
  obtains t where "Γ t = Γ s" "{} c t" "s  T. u  subterms s. u  subterms t"
proof -
  have finite_S: "finite ((funs_term ` T))" using assms(1) by auto

  have 1: "Γ (fresh_pgwt ((funs_term ` T)) (Γ s)) = Γ s"
    using fresh_pgwt_same_type[OF finite_S assms(2)] by auto

  have 2: "{} c fresh_pgwt ((funs_term ` T)) (Γ s)"
    using fresh_pgwt_empty_synth[OF finite_S assms(2)] by auto

  have 3: "v  T. u  subterms v. u  subterms (fresh_pgwt ((funs_term ` T)) (Γ s))"
    using fresh_pgwt_subterm_fresh[OF finite_S assms(2)] assms(3)
          wf_trm_subtermeq subtermeq_imp_funs_term_subset
    by force

  show ?thesis by (rule that[OF 1 2 3])
qed

lemma wt_bij_finite_subst_exists:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)" "wftrms T"
  shows "σ::('fun,'var) subst.
              subst_domain σ = S
             bij_betw σ (subst_domain σ) (subst_range σ)
             subtermsset (subst_range σ)  {t. {} c t} - T
             (s  subst_range σ. u  subst_range σ. (v. v  s  v  u)  s = u)
             wtsubst σ
             wftrms (subst_range σ)"
using assms
proof (induction rule: finite_induct)
  case empty
  have "subst_domain Var = {}"
       "bij_betw Var (subst_domain Var) (subst_range Var)"
       "subtermsset (subst_range Var)  {t. {} c t} - T"
       "s  subst_range Var. u  subst_range Var. (v. v  s  v  u)  s = u"
       "wtsubst Var"
       "wftrms (subst_range Var)"
    unfolding bij_betw_def
    by auto
  thus ?case by (force simp add: subst_domain_def)
next
  case (insert x S)
  then obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subtermsset (subst_range σ)  {t. {} c t} - T"
      "s  subst_range σ. u  subst_range σ. (v. v  s  v  u)  s = u"
      "wtsubst σ" "wftrms (subst_range σ)"
    by (auto simp del: subst_range.simps)

  have *: "finite (T  subst_range σ)"
    using insert.prems(1) insert.hyps(1) σ(1) by simp
  have **: "wftrm (Var x)" by simp
  have ***: "wftrms (T  subst_range σ)" using assms(3) σ(6) by blast
  obtain t where t:
      "Γ t = Γ (Var x)" "{} c t"
      "s  T  subst_range σ. u  subterms s. u  subterms t"
    using wt_fresh_pgwt_term_exists[OF * ** ***] by auto

  obtain θ where θ: "θ  λy. if x = y then t else σ y" by simp

  have t_ground: "fv t = {}" using t(2) pgwt_ground[of t] pgwt_is_empty_synth[of t] by auto
  hence x_dom: "x  subst_domain σ" "x  subst_domain θ" using insert.hyps(2) σ(1) θ by auto
  moreover have "subst_range σ  subtermsset (subst_range σ)" by auto
  hence ground_imgs: "ground (subst_range σ)"
    using σ(3) pgwt_ground pgwt_is_empty_synth
    by force
  ultimately have x_img: "σ x  subst_range σ"
    using ground_subst_dom_iff_img
    by (auto simp add: subst_domain_def)

  have "ground (insert t (subst_range σ))"
    using ground_imgs x_dom t_ground
    by auto
  have θ_dom: "subst_domain θ = insert x (subst_domain σ)"
    using θ t_ground by (auto simp add: subst_domain_def)
  have θ_img: "subst_range θ = insert t (subst_range σ)"
  proof
    show "subst_range θ  insert t (subst_range σ)"
    proof
      fix t' assume "t'  subst_range θ"
      then obtain y where "y  subst_domain θ" "t' = θ y" by auto
      thus "t'  insert t (subst_range σ)" using θ by (auto simp add: subst_domain_def)
    qed
    show "insert t (subst_range σ)  subst_range θ"
    proof
      fix t' assume t': "t'  insert t (subst_range σ)"
      hence "fv t' = {}" using ground_imgs x_img t_ground by auto
      hence "t'  Var x" by auto
      show "t'  subst_range θ"
      proof (cases "t' = t")
        case False
        hence "t'  subst_range σ" using t' by auto
        then obtain y where "σ y  subst_range σ" "t' = σ y" by auto
        hence "y  subst_domain σ" "t'  Var y"
          using ground_subst_dom_iff_img[OF ground_imgs(1)]
          by (auto simp add: subst_domain_def simp del: subst_range.simps)
        hence "x  y" using x_dom by auto
        hence "θ y = σ y" unfolding θ by auto
        thus ?thesis using t'  Var y t' = σ y subst_imgI[of θ y] by auto
      qed (metis subst_imgI θ t'  Var x)
    qed
  qed
  hence θ_ground_img: "ground (subst_range θ)"
    using ground_imgs t_ground
    by auto

  have "subst_domain θ = insert x S" using θ_dom σ(1) by auto
  moreover have "bij_betw θ (subst_domain θ) (subst_range θ)"
  proof (intro bij_betwI')
    fix y z assume *: "y  subst_domain θ" "z  subst_domain θ"
    hence "fv (θ y) = {}" "fv (θ z) = {}" using θ_ground_img by auto
    { assume "θ y = θ z" hence "y = z"
      proof (cases "θ y  subst_range σ  θ z  subst_range σ")
        case True
        hence **: "y  subst_domain σ" "z  subst_domain σ"
          using θ θ_dom True * t(3) by (metis Un_iff term.order_refl insertE)+ 
        hence "y  x" "z  x" using x_dom by auto
        hence "θ y = σ y" "θ z = σ z" using θ by auto
        thus ?thesis using θ y = θ z σ(2) ** unfolding bij_betw_def inj_on_def by auto
      qed (metis θ * θ y = θ z θ_dom ground_imgs(1) ground_subst_dom_iff_img insertE)
    }
    thus "(θ y = θ z) = (y = z)" by auto
  next
    fix y assume "y  subst_domain θ" thus "θ y  subst_range θ" by auto
  next
    fix t assume "t  subst_range θ" thus "z  subst_domain θ. t = θ z" by auto
  qed
  moreover have "subtermsset (subst_range θ)  {t. {} c t}  - T"
  proof -
    { fix s assume "s  t"
      hence "s  {t. {} c t}  - T"
        using t(2,3) 
        by (metis Diff_eq_empty_iff Diff_iff Un_upper1 term.order_refl
                  deduct_synth_subterm mem_Collect_eq) 
    } thus ?thesis using σ(3) θ θ_img by auto
  qed
  moreover have "wtsubst θ" using θ t(1) σ(5) unfolding wtsubst_def by auto
  moreover have "wftrms (subst_range θ)"
    using θ σ(6) t(2) pgwt_is_empty_synth pgwt_wellformed
          wf_trm_subst_range_iff[of σ] wf_trm_subst_range_iff[of θ]
    by metis
  moreover have "ssubst_range θ. usubst_range θ. (v. v  s  v  u)  s = u"
    using σ(4) θ_img t(3) by (auto simp del: subst_range.simps)
  ultimately show ?case by blast
qed

private lemma wt_bij_finite_tatom_subst_exists_single:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)"
  and "x. x  S  Γ (Var x) = TAtom a"
  shows "σ::('fun,'var) subst. subst_domain σ = S
                       bij_betw σ (subst_domain σ) (subst_range σ)
                       subst_range σ  ((λc. Fun c []) `  {c. Γ (Fun c []) = TAtom a 
                                                            public c  arity c = 0}) - T
                       wtsubst σ
                       wftrms (subst_range σ)"
proof -
  let ?U = "{c. Γ (Fun c []) = TAtom a  public c  arity c = 0}"

  obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subst_range σ  ((λc. Fun c []) ` ?U) - T"
    using bij_finite_const_subst_exists'[OF assms(1,2) infinite_typed_consts'[of a]]
    by auto

  { fix x assume "x  subst_domain σ" hence "Γ (Var x) = Γ (σ x)" by auto }
  moreover
  { fix x assume "x  subst_domain σ"
    hence "c  ?U. σ x = Fun c []  arity c = 0" using σ by auto
    hence "Γ (σ x) = TAtom a" "wftrm (σ x)" using assms(3) const_type wf_trmI[of "[]"] by auto
    hence "Γ (Var x) = Γ (σ x)" "wftrm (σ x)" using assms(3) σ(1) by force+
  }
  ultimately have "wtsubst σ" "wftrms (subst_range σ)"
    using wf_trm_subst_range_iff[of σ]
    unfolding wtsubst_def
    by force+
  thus ?thesis using σ by auto
qed

lemma wt_bij_finite_tatom_subst_exists:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)"
  and "x. x  S  a. Γ (Var x) = TAtom a"
  shows "σ::('fun,'var) subst. subst_domain σ = S
                       bij_betw σ (subst_domain σ) (subst_range σ)
                       subst_range σ  ((λc. Fun c []) `  𝒞pub) - T
                       wtsubst σ
                       wftrms (subst_range σ)"
using assms
proof (induction rule: finite_induct)
  case empty
  have "subst_domain Var = {}"
       "bij_betw Var (subst_domain Var) (subst_range Var)"
       "subst_range Var  ((λc. Fun c []) `  𝒞pub) - T"
       "wtsubst Var"
       "wftrms (subst_range Var)"
    unfolding bij_betw_def
    by auto
  thus ?case by (auto simp add: subst_domain_def)
next
  case (insert x S)
  then obtain a where a: "Γ (Var x) = TAtom a" by fastforce

  from insert obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subst_range σ  ((λc. Fun c []) `  𝒞pub) - T" "wtsubst σ"
      "wftrms (subst_range σ)"
    by auto

  let ?S' = "{y  S. Γ (Var y) = TAtom a}"
  let ?T' = "T  subst_range σ"

  have *: "finite (insert x ?S')" using insert by simp
  have **: "finite ?T'" using insert.prems(1) insert.hyps(1) σ(1) by simp
  have ***: "y. y  insert x ?S'  Γ (Var y) = TAtom a" using a by auto

  obtain δ where δ:
      "subst_domain δ = insert x ?S'" "bij_betw δ (subst_domain δ) (subst_range δ)"
      "subst_range δ  ((λc. Fun c []) `  𝒞pub) - ?T'" "wtsubst δ" "wftrms (subst_range δ)"
    using wt_bij_finite_tatom_subst_exists_single[OF * ** ***] const_type_inv[of _ "[]" a]
    by blast

  obtain θ where θ: "θ  λy. if x = y then δ y else σ y" by simp

  have x_dom: "x  subst_domain σ" "x  subst_domain δ" "x  subst_domain θ"
    using insert.hyps(2) σ(1) δ(1) θ by (auto simp add: subst_domain_def)
  moreover have ground_imgs: "ground (subst_range σ)" "ground (subst_range δ)"
    using pgwt_ground σ(3) δ(3) by auto
  ultimately have x_img: "σ x  subst_range σ" "δ x  subst_range δ"
    using ground_subst_dom_iff_img by (auto simp add: subst_domain_def)

  have "ground (insert (δ x) (subst_range σ))" using ground_imgs x_dom by auto
  have θ_dom: "subst_domain θ = insert x (subst_domain σ)"
    using δ(1) θ by (auto simp add: subst_domain_def)
  have θ_img: "subst_range θ = insert (δ x) (subst_range σ)"
  proof
    show "subst_range θ  insert (δ x) (subst_range σ)"
    proof
      fix t assume "t  subst_range θ"
      then obtain y where "y  subst_domain θ" "t = θ y" by auto
      thus "t  insert (δ x) (subst_range σ)" using θ by (auto simp add: subst_domain_def)
    qed
    show "insert (δ x) (subst_range σ)  subst_range θ"
    proof
      fix t assume t: "t  insert (δ x) (subst_range σ)"
      hence "fv t = {}" using ground_imgs x_img(2) by auto
      hence "t  Var x" by auto
      show "t  subst_range θ"
      proof (cases "t = δ x")
        case True thus ?thesis using subst_imgI θ t  Var x by metis
      next
        case False
        hence "t  subst_range σ" using t by auto
        then obtain y where "σ y  subst_range σ" "t = σ y" by auto
        hence "y  subst_domain σ" "t  Var y"
          using ground_subst_dom_iff_img[OF ground_imgs(1)]
          by (auto simp add: subst_domain_def simp del: subst_range.simps)
        hence "x  y" using x_dom by auto
        hence "θ y = σ y" unfolding θ by auto
        thus ?thesis using t  Var y t = σ y subst_imgI[of θ y] by auto
      qed
    qed
  qed
  hence θ_ground_img: "ground (subst_range θ)" using ground_imgs x_img by auto

  have "subst_domain θ = insert x S" using θ_dom σ(1) by auto
  moreover have "bij_betw θ (subst_domain θ) (subst_range θ)"
  proof (intro bij_betwI')
    fix y z assume *: "y  subst_domain θ" "z  subst_domain θ"
    hence "fv (θ y) = {}" "fv (θ z) = {}" using θ_ground_img by auto
    { assume "θ y = θ z" hence "y = z"
      proof (cases "θ y  subst_range σ  θ z  subst_range σ")
        case True
        hence **: "y  subst_domain σ" "z  subst_domain σ"
          using θ θ_dom x_img(2) δ(3) True
          by (metis (no_types) *(1) DiffE Un_upper2 insertE subsetCE,
              metis (no_types) *(2) DiffE Un_upper2 insertE subsetCE)
        hence "y  x" "z  x" using x_dom by auto
        hence "θ y = σ y" "θ z = σ z" using θ by auto
        thus ?thesis using θ y = θ z σ(2) ** unfolding bij_betw_def inj_on_def by auto
      qed (metis θ * θ y = θ z θ_dom ground_imgs(1) ground_subst_dom_iff_img insertE)
    }
    thus "(θ y = θ z) = (y = z)" by auto
  next
    fix y assume "y  subst_domain θ" thus "θ y  subst_range θ" by auto
  next
    fix t assume "t  subst_range θ" thus "z  subst_domain θ. t = θ z" by auto
  qed
  moreover have "subst_range θ  (λc. Fun c []) ` 𝒞pub - T"
    using σ(3) δ(3) θ by (auto simp add: subst_domain_def)
  moreover have "wtsubst θ" using σ(4) δ(4) θ unfolding wtsubst_def by auto
  moreover have "wftrms (subst_range θ)"
    using θ σ(5) δ(5) wf_trm_subst_range_iff[of δ]
          wf_trm_subst_range_iff[of σ] wf_trm_subst_range_iff[of θ]
    by presburger
  ultimately show ?case by blast
qed

theorem wt_sat_if_simple:
  assumes "simple S" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)" "wftrms (trmsst S)"
  and ℐ': "X F. Inequality X F  set S  ineq_model ℐ' X F"
         "ground (subst_range ℐ')"
         "subst_domain ℐ' = {x  varsst S. X F. Inequality X F  set S  x  fvpairs F - set X}"
  and tfr_stp_all: "list_all tfrstp S"
  shows ". interpretationsubst   ( c S, θ)  wtsubst   wftrms (subst_range )"
proof -
  from wfconstr S θ have "wfst {} S" "subst_idem θ" and S_θ_disj: "v  varsst S. θ v = Var v"
    using subst_idemI[of θ] unfolding wfconstr_def wfsubst_def by force+
  
  obtain ::"('fun,'var) subst"
    where : "interpretationsubst " "wtsubst " "subst_range   public_ground_wf_terms"
    using wt_interpretation_exists by blast
  hence ℐ_deduct: "x M. M c  x" and ℐ_wf_trm: "wftrms (subst_range )"
    using pgwt_deducible pgwt_wellformed by fastforce+

  let ?P = "λδ X. subst_domain δ = set X  ground (subst_range δ)"
  let ?Sineqsvars = "{x  varsst S. X F. Inequality X F  set S  x  fvpairs F  x  set X}"
  let ?Strms = "subtermsset (trmsst S)"

  have finite_vars: "finite ?Sineqsvars" "finite ?Strms" "wftrms ?Strms"
    using wf_trm_subtermeq assms(5) by fastforce+

  define Q1 where "Q1 = (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
    x  fvpairs F - set X. a. Γ (Var x) = TAtom a)"

  define Q2 where "Q2 = (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
    f T. Fun f T  subtermsset (trmspairs F)  T = []  (s  set T. s  Var ` set X))"

  define Q1' where "Q1' = (λ(t::('fun,'var) term) (t'::('fun,'var) term) X.
    x  (fv t  fv t') - set X. a. Γ (Var x) = TAtom a)"

  define Q2' where "Q2' = (λ(t::('fun,'var) term) (t'::('fun,'var) term) X.
    f T. Fun f T  subterms t  subterms t'  T = []  (s  set T. s  Var ` set X))"

  have ex_P: "X. δ. ?P δ X" using interpretation_subst_exists' by blast

  have tfr_ineq: "X F. Inequality X F  set S  Q1 F X  Q2 F X"
    using tfr_stp_all Q1_def Q2_def tfrstp_list_all_alt_def[of S] by blast

  have S_fv_bvars_disj: "fvst S  bvarsst S = {}" using wfconstr S θ unfolding wfconstr_def by metis
  hence ineqs_vars_not_bound: "X F x. Inequality X F  set S  x  ?Sineqsvars  x  set X"
    using strand_fv_bvars_disjoint_unfold by blast

  have θ_vars_S_bvars_disj: "(subst_domain θ  range_vars θ)  set X = {}"
    when "Inequality X F  set S" for F X
    using wf_constr_bvars_disj[OF wfconstr S θ]
          strand_fv_bvars_disjointD(1)[OF S_fv_bvars_disj that]
    by blast

  obtain σ::"('fun,'var) subst"
    where σ_fv_dom: "subst_domain σ = ?Sineqsvars"
    and σ_subterm_inj: "subterm_inj_on σ (subst_domain σ)"
    and σ_fresh_pub_img: "subtermsset (subst_range σ)  {t. {} c t} - ?Strms"
    and σ_wt: "wtsubst σ"
    and σ_wf_trm: "wftrms (subst_range σ)"
    using wt_bij_finite_subst_exists[OF finite_vars]
          subst_inj_on_is_bij_betw subterm_inj_on_alt_def'
    by atomize_elim auto

  have σ_bij_dom_img: "bij_betw σ (subst_domain σ) (subst_range σ)"
    by (metis σ_subterm_inj subst_inj_on_is_bij_betw subterm_inj_on_alt_def)

  have "finite (subst_domain σ)" by(metis σ_fv_dom finite_vars(1))
  hence σ_finite_img: "finite (subst_range σ)" using σ_bij_dom_img bij_betw_finite by blast 
  
  have σ_img_subterms: "s  subst_range σ. u  subst_range σ. (v. v  s  v  u)  s = u"
    by (metis σ_subterm_inj subterm_inj_on_alt_def')

  have "subst_range σ  subtermsset (subst_range σ)" by auto
  hence "subst_range σ  public_ground_wf_terms - ?Strms"
      and σ_pgwt_img:
        "subst_range σ  public_ground_wf_terms"
        "subtermsset (subst_range σ)  public_ground_wf_terms"
    using σ_fresh_pub_img pgwt_is_empty_synth by blast+

  have σ_img_ground: "ground (subst_range σ)"
    using σ_pgwt_img pgwt_ground by auto
  hence σ_inj: "inj σ"
    using σ_bij_dom_img subst_inj_is_bij_betw_dom_img_if_ground_img by auto

  have σ_ineqs_fv_dom: "X F. Inequality X F  set S  fvpairs F - set X  subst_domain σ"
    using σ_fv_dom by fastforce

  have σ_dom_bvars_disj: "X F. Inequality X F  set S  subst_domain σ  set X = {}"
    using ineqs_vars_not_bound σ_fv_dom by fastforce
  
  have ℐ'1: "X F δ. Inequality X F  set S  fvpairs F - set X  subst_domain ℐ'"
    using ℐ'(3) ineqs_vars_not_bound by fastforce
  
  have ℐ'2: "X F. Inequality X F  set S  subst_domain ℐ'  set X = {}"
    using ℐ'(3) ineqs_vars_not_bound by blast
  
  have doms_eq: "subst_domain ℐ' = subst_domain σ" using ℐ'(3) σ_fv_dom by simp

  have σ_ineqs_neq: "ineq_model σ X F" when "Inequality X F  set S" for X F
  proof -
    obtain a::"'fun" where a: "a  (funs_term ` subtermsset (subst_range σ))"
      using exists_fun_notin_funs_terms[OF subterms_union_finite[OF σ_finite_img]]
      by atomize_elim auto
    hence a': "T. Fun a T  subtermsset (subst_range σ)"
              "S. Fun a []  set (Fun a []#S)" "Fun a []  Var ` set X"
      by (meson a UN_I term.set_intros(1), auto)

    define t where "t  Fun a (Fun a []#map fst F)"
    define t' where "t'  Fun a (Fun a []#map snd F)"

    note F_in = that

    have t_fv: "fv t  fv t'  fvpairs F"
      unfolding t_def t'_def by force

    have t_subterms: "subterms t  subterms t'  subtermsset (trmspairs F)  {t, t', Fun a []}"
      unfolding t_def t'_def by force

    have "t  δ  σ  t'  δ  σ" when "?P δ X" for δ
    proof -
      have tfr_assms: "Q1 F X  Q2 F X" using tfr_ineq F_in by metis
  
      have "Q1 F X  x  fvpairs F - set X. c. σ x = Fun c []"
      proof
        fix x assume "Q1 F X" and x: "x  fvpairs F - set X"
        then obtain a where "Γ (Var x) = TAtom a" unfolding Q1_def by atomize_elim auto
        hence a: "Γ (σ x) = TAtom a" using σ_wt unfolding wtsubst_def by simp
        
        have "x  subst_domain σ" using σ_ineqs_fv_dom x F_in by auto
        then obtain f T where fT: "σ x = Fun f T" by (meson σ_img_ground ground_img_obtain_fun)
        hence "T = []" using σ_wf_trm a TAtom_term_cases by fastforce
        thus "c. σ x = Fun c []" using fT by metis
      qed
      hence 1: "Q1 F X  x  (fv t  fv t') - set X. c. σ x = Fun c []"
        using t_fv by auto
  
      have 2: "¬Q1 F X  Q2 F X" by (metis tfr_assms)
  
      have 3: "subst_domain σ  set X = {}" using σ_dom_bvars_disj F_in by auto

      have 4: "subtermsset (subst_range σ)  (subterms t  subterms t') = {}"
      proof -
        define M1 where "M1  {t, t', Fun a []}"
        define M2 where "M2  ?Strms"

        have "subtermsset (trmspairs F)  M2"
          using F_in unfolding M2_def by force
        moreover have "subterms t  subterms t'  subtermsset (trmspairs F)  M1"
          using t_subterms unfolding M1_def by blast
        ultimately have *: "subterms t  subterms t'  M2  M1"
          by auto

        have "subtermsset (subst_range σ)  M1 = {}"
             "subtermsset (subst_range σ)  M2 = {}"
          using a' σ_fresh_pub_img
          unfolding t_def t'_def M1_def M2_def
          by blast+
        thus ?thesis using * by blast
      qed
  
      have 5: "(fv t  fv t') - subst_domain σ  set X"
        using σ_ineqs_fv_dom[OF F_in] t_fv
        by auto
  
      have 6: "δ. ?P δ X  t  δ  ℐ'  t'  δ  ℐ'"
        by (metis t_def t'_def ℐ'(1) F_in ineq_model_singleE ineq_model_single_iff)
  
      have 7: "fv t  fv t' - set X  subst_domain ℐ'" using ℐ'1 F_in t_fv by force
  
      have 8: "subst_domain ℐ'  set X = {}" using ℐ'2 F_in by auto

      have 9: "Q1' t t' X" when "Q1 F X"
        using that t_fv
        unfolding Q1_def Q1'_def t_def t'_def
        by blast

      have 10: "Q2' t t' X" when "Q2 F X" unfolding Q2'_def
      proof (intro allI impI)
        fix f T assume "Fun f T  subterms t  subterms t'"
        moreover {
          assume "Fun f T  subtermsset (trmspairs F)"
          hence "T = []  (sset T. s  Var ` set X)" by (metis Q2_def that)
        } moreover {
          assume "Fun f T = t" hence "T = []  (sset T. s  Var ` set X)"
            unfolding t_def using a'(2,3) by simp
        } moreover {
          assume "Fun f T = t'" hence "T = []  (sset T. s  Var ` set X)"
            unfolding t'_def using a'(2,3) by simp
        } moreover {
          assume "Fun f T = Fun a []" hence "T = []  (sset T. s  Var ` set X)" by simp
        } ultimately show "T = []  (sset T. s  Var ` set X)" using t_subterms by blast
      qed

      note 11 = σ_subterm_inj σ_img_ground 3 4 5
  
      note 12 = 6 7 8 ℐ'(2) doms_eq
  
      show "t  δ  σ  t'  δ  σ"
        using 1 2 9 10 that sat_ineq_subterm_inj_subst[OF 11 _ 12] 
        unfolding Q1'_def Q2'_def by metis
    qed
    thus ?thesis by (metis t_def t'_def ineq_model_singleI ineq_model_single_iff)
  qed

  have σ_ineqs_fv_dom': "fvpairs (F pairs δ)  subst_domain σ"
    when "Inequality X F  set S" and "?P δ X" for F δ X
    using σ_ineqs_fv_dom[OF that(1)]
  proof (induction F)
    case (Cons g G)
    obtain t t' where g: "g = (t,t')" by (metis surj_pair)
    hence "fvpairs (g#G pairs δ)  = fv (t  δ)  fv (t'  δ)  fvpairs (G pairs δ)"
          "fvpairs (g#G) = fv t  fv t'  fvpairs G"
      by (simp_all add: subst_apply_pairs_def)
    moreover have "fv (t  δ) = fv t - subst_domain δ" "fv (t'  δ) = fv t' - subst_domain δ"
      using g that(2) by (simp_all add: subst_fv_unfold_ground_img range_vars_alt_def)
    moreover have "fvpairs (G pairs δ)  subst_domain σ" using Cons by auto
    ultimately show ?case using Cons.prems that(2) by auto
  qed (simp add: subst_apply_pairs_def)

  have σ_ineqs_ground: "fvpairs ((F pairs δ) pairs σ) = {}"
    when "Inequality X F  set S" and "?P δ X" for F δ X
    using σ_ineqs_fv_dom'[OF that]
  proof (induction F)
    case (Cons g G)
    obtain t t' where g: "g = (t,t')" by (metis surj_pair)
    hence "fv (t  δ)  subst_domain σ" "fv (t'  δ)  subst_domain σ"
      using Cons.prems by (auto simp add: subst_apply_pairs_def)
    hence "fv (t  δ  σ) = {}" "fv (t'  δ  σ) = {}"
      using subst_fv_dom_ground_if_ground_img[OF _ σ_img_ground] by metis+
    thus ?case using g Cons by (auto simp add: subst_apply_pairs_def)
  qed (simp add: subst_apply_pairs_def)
 
  from σ_pgwt_img σ_ineqs_neq have σ_deduct: "M c σ x" when "x  subst_domain σ" for x M
    using that pgwt_deducible by fastforce

  { fix M::"('fun,'var) terms"
    have "M; Sc (θ s σ s )"
      using wfst {} S simple S S_θ_disj σ_ineqs_neq σ_ineqs_fv_dom' θ_vars_S_bvars_disj
    proof (induction S arbitrary: M rule: wfst_simple_induct)
      case (ConsSnd v S)
      hence S_sat: "M; Sc (θ s σ s )" and "θ v = Var v" by auto
      hence *: "M. M c Var v  (θ s σ s )"
        using ℐ_deduct σ_deduct
        by (metis ideduct_synth_subst_apply eval_term.simps(1)
                  subst_subst_compose trm_subst_ident')

      define M' where "M'  M  (ikst S set θ s σ s )"

      have "t  set [Var v]. M' c t  (θ s σ s )" using *[of M'] by simp
      thus ?case
        using strand_sem_append(1)[OF S_sat, of "[Send1 (Var v)]", unfolded M'_def[symmetric]]
              strand_sem_c.simps(1)[of M'] strand_sem_c.simps(2)[of M' "[Var v]" "[]"]
        by presburger
    next
      case (ConsIneq X F S)
      have dom_disj: "subst_domain θ  fvpairs F = {}"
        using ConsIneq.prems(1) subst_dom_vars_in_subst
        by force
      hence *: "F pairs θ = F" by blast

      have **: "ineq_model σ X F" by (meson ConsIneq.prems(2) in_set_conv_decomp)

      have "x. x  varsst S  x  varsst (S@[Inequality X F])"
           "x. x  set S  x  set (S@[Inequality X F])" by auto
      hence IH: "M; Sc (θ s σ s )" by (metis ConsIneq.IH ConsIneq.prems(1,2,3,4))

      have "ineq_model (σ s ) X F"
      proof -
        have "fvpairs (F pairs δ)  subst_domain σ" when "?P δ X" for δ
          using ConsIneq.prems(3)[OF _ that] by simp
        hence "fvpairs F - set X  subst_domain σ"
          using fvpairs_subst_subset ex_P
          by