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 (metis Diff_subset_conv Un_commute)
        thus ?thesis by (metis ineq_model_ground_subst[OF _ σ_img_ground **])
      qed
      hence "ineq_model (θ s σ s ) X F"
        using * ineq_model_subst' subst_compose_assoc ConsIneq.prems(4)
        by (metis UnCI list.set_intros(1) set_append)
      thus ?case using IH by (auto simp add: ineq_model_def)
    qed auto
  }
  moreover have "wtsubst (θ s σ s )" "wftrms (subst_range (θ s σ s ))"
    by (metis wt_subst_compose wtsubst θ wtsubst σ wtsubst ,
        metis assms(4) ℐ_wf_trm σ_wf_trm wf_trm_subst subst_img_comp_subset')
  ultimately show ?thesis
    using interpretation_comp(1)[OF interpretationsubst , of "θ s σ"]
          subst_idem_support[OF subst_idem θ, of "σ s "] subst_compose_assoc
    unfolding constr_sem_c_def by metis
qed
end


subsubsection ‹Theorem: Type-flaw resistant constraints are well-typed satisfiable (composition-only)›
text ‹
  There exists well-typed models of satisfiable type-flaw resistant constraints in the
  semantics where the intruder is limited to composition only (i.e., he cannot perform
  decomposition/analysis of deducible messages).
›
theorem wt_attack_if_tfr_attack:
  assumes "interpretationsubst "
    and " c S, θ"
    and "wfconstr S θ"
    and "wtsubst θ"
    and "tfrst S"
    and "wftrms (trmsst S)"
    and "wftrms (subst_range θ)"
  obtains τ where "interpretationsubst τ"
    and "τ c S, θ"
    and "wtsubst τ"
    and "wftrms (subst_range τ)"
proof -
  have tfr: "tfrset (trmsst (LI_preproc S))" "wftrms (trmsst (LI_preproc S))"
            "list_all tfrstp (LI_preproc S)"
    using assms(5,6) LI_preproc_preserves_tfr 
    unfolding tfrst_def by (metis, metis LI_preproc_trms_eq, metis)
  have wf_constr: "wfconstr (LI_preproc S) θ" by (metis LI_preproc_preserves_wellformedness assms(3))
  obtain S' θ' where *: "simple S'" "(LI_preproc S,θ) * (S',θ')" "{}; S'c "
    using LI_completeness[OF assms(3,2)] unfolding constr_sem_c_def
    by (meson term.order_refl)
  have **: "wfconstr S' θ'" "wtsubst θ'" "list_all tfrstp S'" "wftrms (trmsst S')" "wftrms (subst_range θ')" 
    using LI_preserves_welltypedness[OF *(2) wf_constr assms(4,7) tfr]
          LI_preserves_wellformedness[OF *(2) wf_constr]
          LI_preserves_tfr[OF *(2) wf_constr assms(4,7) tfr]
    by metis+

  define A where "A  {x  varsst S'. X F. Inequality X F  set S'  x  fvpairs F  x  set X}"
  define B where "B  UNIV - A"

  let ?ℐ = "rm_vars B "

  have grℐ: "ground (subst_range )" "ground (subst_range ?ℐ)"
    using assms(1) rm_vars_img_subset[of B ] by (auto simp add: subst_domain_def)

  { fix X F
    assume "Inequality X F  set S'"
    hence *: "ineq_model  X F"
      using strand_sem_c_imp_ineq_model[OF *(3)]
      by (auto simp del: subst_range.simps)
    hence "ineq_model ?ℐ X F"
    proof -
      { fix δ
        assume 1: "subst_domain δ = set X" "ground (subst_range δ)"
            and 2: "list_ex (λf. fst f  δ s   snd f  δ s ) F"
        have "list_ex (λf. fst f  δ s rm_vars B   snd f  δ s rm_vars B ) F" using 2
        proof (induction F)
          case (Cons g G)
          obtain t t' where g: "g = (t,t')" by (metis surj_pair)
          thus ?case
            using Cons Unifier_ground_rm_vars[OF grℐ(1), of "t  δ" B "t'  δ"]
            by auto
        qed simp
      } thus ?thesis using * unfolding ineq_model_def list_ex_iff case_prod_unfold by simp
    qed
  } moreover have "subst_domain  = UNIV" using assms(1) by metis
  hence "subst_domain ?ℐ = A" using rm_vars_dom[of B ] B_def by blast
  ultimately obtain τ where
      "interpretationsubst τ" "τ c S', θ'" "wtsubst τ" "wftrms (subst_range τ)"
    using wt_sat_if_simple[OF *(1) **(1,2,5,4) _ grℐ(2) _ **(3)] A_def
    by (auto simp del: subst_range.simps)
  thus ?thesis using that LI_soundness[OF assms(3) *(2)] by metis
qed

text ‹
  Contra-positive version: if a type-flaw resistant constraint does not have a well-typed model
  then it is unsatisfiable
›
corollary secure_if_wt_secure:
  assumes "¬(τ. interpretationsubst τ  (τ c S, θ)  wtsubst τ)"
  and     "wfconstr S θ" "wtsubst θ" "tfrst S"
  and     "wftrms (trmsst S)" "wftrms (subst_range θ)"
  shows "¬(. interpretationsubst   ( c S, θ))"
using wt_attack_if_tfr_attack[OF _ _ assms(2,3,4,5,6)] assms(1) by metis

end


subsection ‹Lifting the Composition-Only Typing Result to the Full Intruder Model›
context typing_result
begin

subsubsection ‹Analysis Invariance›
definition (in typed_model) Ana_invar_subst where
  "Ana_invar_subst  
    (f T K M δ. Fun f T  (subtermsset ) 
                 Ana (Fun f T) = (K, M)  Ana (Fun f T  δ) = (K list δ, M list δ))"

lemma (in typed_model) Ana_invar_subst_subset:
  assumes "Ana_invar_subst M" "N  M"
  shows "Ana_invar_subst N"
using assms unfolding Ana_invar_subst_def by blast

lemma (in typed_model) Ana_invar_substD:
  assumes "Ana_invar_subst "
  and "Fun f T  subtermsset " "Ana (Fun f T) = (K, M)"
  shows "Ana (Fun f T  ) = (K list , M list )"
using assms Ana_invar_subst_def by blast

end


subsubsection ‹Preliminary Definitions›
text ‹Strands extended with "decomposition steps"›
datatype (funsestp: 'a, varsestp: 'b) extstrand_step =
  Step   "('a,'b) strand_step"
| Decomp "('a,'b) term"

context typing_result
begin

context
begin
private fun trmsestp where
  "trmsestp (Step x) = trmsstp x"
| "trmsestp (Decomp t) = {t}"

private abbreviation trmsest where "trmsest S  (trmsestp ` set S)"

private type_synonym ('a,'b) extstrand = "('a,'b) extstrand_step list"
private type_synonym ('a,'b) extstrands = "('a,'b) extstrand set"

private definition decomp::"('fun,'var) term  ('fun,'var) strand" where
  "decomp t  (case (Ana t) of (K,T)  [send⟨[t]st,send⟨Kst,receive⟨Tst])"

private fun to_st where
  "to_st [] = []"
| "to_st (Step x#S) = x#(to_st S)"
| "to_st (Decomp t#S) = (decomp t)@(to_st S)"

private fun to_est where
  "to_est [] = []"
| "to_est (x#S) = Step x#to_est S"

private abbreviation "ikest A  ikst (to_st A)"
private abbreviation "wfest V A  wfst V (to_st A)"
private abbreviation "assignment_rhsest A  assignment_rhsst (to_st A)"
private abbreviation "varsest A  varsst (to_st A)"
private abbreviation "wfrestrictedvarsest A  wfrestrictedvarsst (to_st A)"
private abbreviation "bvarsest A  bvarsst (to_st A)"
private abbreviation "fvest A  fvst (to_st A)"
private abbreviation "funsest A  funsst (to_st A)"

private definition wfsts'::"('fun,'var) strands  ('fun,'var) extstrand  bool" where
  "wfsts' 𝒮 𝒜  (S  𝒮. wfst (wfrestrictedvarsest 𝒜) (dualst S)) 
                 (S  𝒮. S'  𝒮. fvst S  bvarsst S' = {}) 
                 (S  𝒮. fvst S  bvarsest 𝒜 = {}) 
                 (S  𝒮. fvst (to_st 𝒜)  bvarsst S = {})"

private definition wfsts::"('fun,'var) strands  bool" where
  "wfsts 𝒮  (S  𝒮. wfst {} (dualst S))  (S  𝒮. S'  𝒮. fvst S  bvarsst S' = {})"

private inductive well_analyzed::"('fun,'var) extstrand  bool" where
  Nil[simp]: "well_analyzed []"
| Step: "well_analyzed A  well_analyzed (A@[Step x])"
| Decomp: "well_analyzed A; t  subtermsset (ikest A  assignment_rhsest A) - (Var ` 𝒱)
     well_analyzed (A@[Decomp t])"

private fun subst_apply_extstrandstep (infix "estp" 51) where
  "subst_apply_extstrandstep (Step x) θ = Step (x stp θ)"
| "subst_apply_extstrandstep (Decomp t) θ = Decomp (t  θ)"

private lemma subst_apply_extstrandstep'_simps[simp]:
  "(Step (send⟨tsst)) estp θ = Step (send⟨ts list θst)"
  "(Step (receive⟨tsst)) estp θ = Step (receive⟨ts list θst)"
  "(Step (a: t  t'st)) estp θ = Step (a: (t  θ)  (t'  θ)st)"
  "(Step (X⟨∨≠: Fst)) estp θ = Step (X⟨∨≠: (F pairs rm_vars (set X) θ)st)"
by simp_all

private lemma varsestp_subst_apply_simps[simp]:
  "varsestp ((Step (send⟨tsst)) estp θ) = fvset (set ts set θ)"
  "varsestp ((Step (receive⟨tsst)) estp θ) = fvset (set ts set θ)"
  "varsestp ((Step (a: t  t'st)) estp θ) = fv (t  θ)  fv (t'  θ)"
  "varsestp ((Step (X⟨∨≠: Fst)) estp θ) = set X  fvpairs (F pairs rm_vars (set X) θ)"
by auto

private definition subst_apply_extstrand (infix "est" 51) where "S est θ  map (λx. x estp θ) S"

private abbreviation updatest::"('fun,'var) strands  ('fun,'var) strand  ('fun,'var) strands"
where
  "updatest 𝒮 S  (case S of Nil  𝒮 - {S} | Cons _ S'  insert S' (𝒮 - {S}))"

private inductive_set decompsest::
  "('fun,'var) terms  ('fun,'var) terms  ('fun,'var) subst  ('fun,'var) extstrands"
(* ℳ: intruder knowledge
   𝒩: additional messages
*)
for  and 𝒩 and  where
  Nil: "[]  decompsest  𝒩 "
| Decomp: "𝒟  decompsest  𝒩 ; Fun f T  subtermsset (  𝒩);
            Ana (Fun f T) = (K,M); M  [];
            (  ikest 𝒟) set  c Fun f T  ;
            k. k  set K  (  ikest 𝒟) set  c k  
             𝒟@[Decomp (Fun f T)]  decompsest  𝒩 "

private fun decomp_rmest::"('fun,'var) extstrand  ('fun,'var) extstrand" where
  "decomp_rmest [] = []"
| "decomp_rmest (Decomp t#S) = decomp_rmest S"
| "decomp_rmest (Step x#S) = Step x#(decomp_rmest S)"

private inductive semest_d::"('fun,'var) terms  ('fun,'var) subst  ('fun,'var) extstrand  bool"
where
  Nil[simp]: "semest_d M0  []"
| Send: "semest_d M0  S  t  set ts. (ikest S  M0) set   t  
           semest_d M0  (S@[Step (send⟨tsst)])"
| Receive: "semest_d M0  S  semest_d M0  (S@[Step (receive⟨tst)])"
| Equality: "semest_d M0  S  t   = t'    semest_d M0  (S@[Step (a: t  t'st)])"
| Inequality: "semest_d M0  S
     ineq_model  X F
     semest_d M0  (S@[Step (X⟨∨≠: Fst)])"
| Decompose: "semest_d M0  S  (ikest S  M0) set   t    Ana t = (K, M)
     (k. k  set K  (ikest S  M0) set   k  )  semest_d M0  (S@[Decomp t])"

private inductive semest_c::"('fun,'var) terms  ('fun,'var) subst  ('fun,'var) extstrand  bool"
where
  Nil[simp]: "semest_c M0  []"
| Send: "semest_c M0  S  t  set ts. (ikest S  M0) set  c t  
           semest_c M0  (S@[Step (send⟨tsst)])"
| Receive: "semest_c M0  S  semest_c M0  (S@[Step (receive⟨tst)])"
| Equality: "semest_c M0  S  t   = t'    semest_c M0  (S@[Step (a: t  t'st)])"
| Inequality: "semest_c M0  S
     ineq_model  X F
     semest_c M0  (S@[Step (X⟨∨≠: Fst)])"
| Decompose: "semest_c M0  S  (ikest S  M0) set  c t    Ana t = (K, M)
     (k. k  set K  (ikest S  M0) set  c k  )  semest_c M0  (S@[Decomp t])"


subsubsection ‹Preliminary Lemmata›
private lemma wfsts_wfsts':
  "wfsts 𝒮 = wfsts' 𝒮 []"
by (simp add: wfsts_def wfsts'_def)

private lemma decomp_ik:
  assumes "Ana t = (K,M)"
  shows "ikst (decomp t) = set M"
using ik_rcv_map ik_rcv_map'
by (auto simp add: decomp_def inv_def assms)

private lemma decomp_assignment_rhs_empty:
  assumes "Ana t = (K,M)"
  shows "assignment_rhsst (decomp t) = {}"
by (auto simp add: decomp_def inv_def assms)

private lemma decomp_tfrstp:
  "list_all tfrstp (decomp t)"
by (auto simp add: decomp_def list_all_def)

private lemma trmsest_ikI:
  "t  ikest A  t  subtermsset (trmsest A)"
proof (induction A rule: to_st.induct)
  case (2 x S) thus ?case by (cases x) auto
next
  case (3 t' A)
  obtain K M where Ana: "Ana t' = (K,M)" by (metis surj_pair)
  show ?case using 3 decomp_ik[OF Ana] Ana_subterm[OF Ana] by auto
qed simp

private lemma trmsest_ik_assignment_rhsI:
  "t  ikest A  assignment_rhsest A  t  subtermsset (trmsest A)"
proof (induction A rule: to_st.induct)
  case (2 x S) thus ?case
  proof (cases x)
    case (Equality ac t t') thus ?thesis using 2 by (cases ac) auto
  qed auto
next
  case (3 t' A)
  obtain K M where Ana: "Ana t' = (K,M)" by (metis surj_pair)
  show ?case
    using 3 decomp_ik[OF Ana] decomp_assignment_rhs_empty[OF Ana] Ana_subterm[OF Ana]
    by auto
qed simp

private lemma trmsest_ik_subtermsI:
  assumes "t  subtermsset (ikest A)"
  shows "t  subtermsset (trmsest A)"
proof -
  obtain t' where "t'  ikest A" "t  t'" using trmsest_ikI assms by auto
  thus ?thesis by (meson contra_subsetD in_subterms_subset_Union trmsest_ikI)
qed

private lemma trmsestD:
  assumes "t  trmsest A"
  shows "t  trmsst (to_st A)"
using assms
proof (induction A)
  case (Cons a A)
  obtain K M where Ana: "Ana t = (K,M)" by (metis surj_pair)
  hence "t  trmsst (decomp t)" unfolding decomp_def by force
  thus ?case using Cons.IH Cons.prems by (cases a) auto
qed simp

private lemma subst_apply_extstrand_nil[simp]:
  "[] est θ = []"
by (simp add: subst_apply_extstrand_def)

private lemma subst_apply_extstrand_singleton[simp]:
  "[Step (receive⟨tsst)] est θ = [Step (Receive (ts list θ))]"
  "[Step (send⟨tsst)] est θ = [Step (Send (ts list θ))]"
  "[Step (a: t  t'st)] est θ = [Step (Equality a (t  θ) (t'  θ))]"
  "[Decomp t] est θ = [Decomp (t  θ)]"
unfolding subst_apply_extstrand_def by auto

private lemma extstrand_subst_hom:
  "(S@S') est θ = (S est θ)@(S' est θ)" "(x#S) est θ = (x estp θ)#(S est θ)"
unfolding subst_apply_extstrand_def by auto

private lemma decomp_vars:
  "wfrestrictedvarsst (decomp t) = fv t" "varsst (decomp t) = fv t" "bvarsst (decomp t) = {}"
  "fvst (decomp t) = fv t"
proof -
  obtain K M where Ana: "Ana t = (K,M)" by (metis surj_pair)
  hence "decomp t = [send⟨[t]st,Send K,Receive M]"
    unfolding decomp_def by simp
  moreover have "(set (map fv K)) = fvset (set K)" "(set (map fv M)) = fvset (set M)" by auto
  moreover have "fvset (set K)  fv t" "fvset (set M)  fv t"
    using Ana_subterm[OF Ana(1)] Ana_keys_fv[OF Ana(1)]
    by (simp_all add: UN_least psubsetD subtermeq_vars_subset)
  ultimately show
      "wfrestrictedvarsst (decomp t) = fv t" "varsst (decomp t) = fv t" "bvarsst (decomp t) = {}"
      "fvst (decomp t) = fv t"
    by auto
qed

private lemma bvarsest_cons: "bvarsest (x#X) = bvarsest [x]  bvarsest X"
by (cases x) auto

private lemma bvarsest_append: "bvarsest (A@B) = bvarsest A  bvarsest B"
proof (induction A)
  case (Cons x A) thus ?case using bvarsest_cons[of x "A@B"] bvarsest_cons[of x A] by force
qed simp

private lemma fvest_cons: "fvest (x#X) = fvest [x]  fvest X"
by (cases x) auto

private lemma fvest_append: "fvest (A@B) = fvest A  fvest B"
proof (induction A)
  case (Cons x A) thus ?case using fvest_cons[of x "A@B"] fvest_cons[of x A] by auto
qed simp

private lemma bvars_decomp: "bvarsest (A@[Decomp t]) = bvarsest A" "bvarsest (Decomp t#A) = bvarsest A"
using bvarsest_append decomp_vars(3) by fastforce+

private lemma bvars_decomp_rm: "bvarsest (decomp_rmest A) = bvarsest A"
using bvars_decomp by (induct A rule: decomp_rmest.induct) simp_all+

private lemma fv_decomp_rm: "fvest (decomp_rmest A)  fvest A"
by (induct A rule: decomp_rmest.induct) auto

private lemma ik_assignment_rhs_decomp_fv:
  assumes "t  subtermsset (ikest A  assignment_rhsest A)"
  shows "fvest (A@[Decomp t]) = fvest A"
proof -
  have "fvest (A@[Decomp t]) = fvest A  fv t" using fvest_append decomp_vars by simp
  moreover have "fvset (ikest A  assignment_rhsest A)  fvest A" by force
  moreover have "fv t  fvset (ikest A  assignment_rhsest A)"
    using fv_subset_subterms[OF assms(1)] by simp
  ultimately show ?thesis by blast
qed

private lemma wfrestrictedvarsest_decomp_rmest_subset:
  "wfrestrictedvarsest (decomp_rmest A)  wfrestrictedvarsest A"
by (induct A rule: decomp_rmest.induct) auto+

private lemma wfrestrictedvarsest_eq_wfrestrictedvarsst:
  "wfrestrictedvarsest A = wfrestrictedvarsst (to_st A)"
by simp

private lemma decomp_set_unfold:
  assumes "Ana t = (K, M)"
  shows "set (decomp t) = {send⟨[t]st,send⟨Kst,receive⟨Mst}"
using assms unfolding decomp_def by auto

private lemma ikest_finite: "finite (ikest A)"
by (rule finite_ikst)

private lemma assignment_rhsest_finite: "finite (assignment_rhsest A)"
by (rule finite_assignment_rhsst)

private lemma to_est_append: "to_est (A@B) = to_est A@to_est B"
by (induct A rule: to_est.induct) auto

private lemma to_st_to_est_inv: "to_st (to_est A) = A"
by (induct A rule: to_est.induct) auto

private lemma to_st_append: "to_st (A@B) = (to_st A)@(to_st B)"
by (induct A rule: to_st.induct) auto

private lemma to_st_cons: "to_st (a#B) = (to_st [a])@(to_st B)"
using to_st_append[of "[a]" B] by simp

private lemma wfrestrictedvarsest_split:
  "wfrestrictedvarsest (x#S) = wfrestrictedvarsest [x]  wfrestrictedvarsest S"
  "wfrestrictedvarsest (S@S') = wfrestrictedvarsest S  wfrestrictedvarsest S'"
using to_st_cons[of x S] to_st_append[of S S'] by auto

private lemma ikest_append: "ikest (A@B) = ikest A  ikest B"
by (metis ik_append to_st_append)

private lemma assignment_rhsest_append:
  "assignment_rhsest (A@B) = assignment_rhsest A  assignment_rhsest B"
by (metis assignment_rhs_append to_st_append)

private lemma ikest_cons: "ikest (a#A) = ikest [a]  ikest A"
by (metis ik_append to_st_cons) 

private lemma ikest_append_subst:
  "ikest (A@B est θ) = ikest (A est θ)  ikest (B est θ)"
  "ikest (A@B) set θ = (ikest A set θ)  (ikest B set θ)"
by (metis ikest_append extstrand_subst_hom(1), simp add: image_Un to_st_append)

private lemma assignment_rhsest_append_subst:
  "assignment_rhsest (A@B est θ) = assignment_rhsest (A est θ)  assignment_rhsest (B est θ)"
  "assignment_rhsest (A@B) set θ = (assignment_rhsest A set θ)  (assignment_rhsest B set θ)"
by (metis assignment_rhsest_append extstrand_subst_hom(1), use assignment_rhsest_append in blast)

private lemma ikest_cons_subst:
  "ikest (a#A est θ) = ikest ([a estp θ])  ikest (A est θ)"
  "ikest (a#A) set θ = (ikest [a] set θ)  (ikest A set θ)"
by (metis ikest_cons extstrand_subst_hom(2), metis image_Un ikest_cons)

private lemma decomp_rmest_append: "decomp_rmest (S@S') = (decomp_rmest S)@(decomp_rmest S')"
by (induct S rule: decomp_rmest.induct) auto

private lemma decomp_rmest_single[simp]:
  "decomp_rmest [Step (send⟨tsst)] = [Step (send⟨tsst)]"
  "decomp_rmest [Step (receive⟨tsst)] = [Step (receive⟨tsst)]"
  "decomp_rmest [Decomp t] = []"
by auto

private lemma decomp_rmest_ik_subset: "ikest (decomp_rmest S)  ikest S"
proof (induction S rule: decomp_rmest.induct)
  case (3 x S) thus ?case by (cases x) auto
qed auto

private lemma decompsest_ik_subset: "D  decompsest M N   ikest D  subtermsset (M  N)"
proof (induction D rule: decompsest.induct)
  case (Decomp D f T K M')
  have "ikst (decomp (Fun f T))  subterms (Fun f T)"
       "ikst (decomp (Fun f T)) = ikest [Decomp (Fun f T)]"
    using decomp_ik[OF Decomp.hyps(3)] Ana_subterm[OF Decomp.hyps(3)]
    by auto
  hence "ikst (to_st [Decomp (Fun f T)])  subtermsset (M  N)"
    using in_subterms_subset_Union[OF Decomp.hyps(2)]
    by blast
  thus ?case using ikest_append[of D "[Decomp (Fun f T)]"] using Decomp.IH by auto
qed simp

private lemma decompsest_decomp_rmest_empty: "D  decompsest M N   decomp_rmest D = []"
by (induct D rule: decompsest.induct) (auto simp add: decomp_rmest_append)

private lemma decompsest_append:
  assumes "A  decompsest S N " "B  decompsest S N "
  shows "A@B  decompsest S N "
using assms(2)
proof (induction B rule: decompsest.induct)
  case Nil show ?case using assms(1) by simp
next
  case (Decomp B f X K T)
  hence "S  ikest B set   S  ikest (A@B) set " using ikest_append by auto
  thus ?case
    using decompsest.Decomp[OF Decomp.IH(1) Decomp.hyps(2,3,4)]
          ideduct_synth_mono[OF Decomp.hyps(5)]
          ideduct_synth_mono[OF Decomp.hyps(6)]
    by auto
qed

private lemma decompsest_subterms:
  assumes "A'  decompsest M N "
  shows "subtermsset (ikest A')  subtermsset (M  N)"
using assms
proof (induction A' rule: decompsest.induct)
  case (Decomp D f X K T)
  hence "Fun f X  subtermsset (M  N)" by auto
  hence "subtermsset (set X)  subtermsset (M  N)"
    using in_subterms_subset_Union[of "Fun f X" "M  N"] params_subterms_Union[of X f]
    by blast
  moreover have "ikst (to_st [Decomp (Fun f X)]) = set T" using Decomp.hyps(3) decomp_ik by simp
  hence "subtermsset (ikst (to_st [Decomp (Fun f X)]))  subtermsset (set X)"
    using Ana_fun_subterm[OF Decomp.hyps(3)] by auto
  ultimately show ?case
    using ikest_append[of D "[Decomp (Fun f X)]"] Decomp.IH
    by auto
qed simp

private lemma decompsest_assignment_rhs_empty:
  assumes "A'  decompsest M N "
  shows "assignment_rhsest A' = {}"
using assms
by (induction A' rule: decompsest.induct)
   (simp_all add: decomp_assignment_rhs_empty assignment_rhsest_append) 

private lemma decompsest_finite_ik_append:
  assumes "finite M" "M  decompsest A N "
  shows "D  decompsest A N . ikest D = (m  M. ikest m)"
using assms
proof (induction M rule: finite_induct)
  case empty
  moreover have "[]  decompsest A N " "ikst (to_st []) = {}" using decompsest.Nil by auto
  ultimately show ?case by blast
next
  case (insert m M)
  then obtain D where "D  decompsest A N " "ikest D = (mM. ikst (to_st m))" by atomize_elim auto
  moreover have "m  decompsest A N " using insert.prems(1) by blast
  ultimately show ?case using decompsest_append[of D A N  m] ikest_append[of D m] by blast
qed

private lemma decomp_snd_exists[simp]: "D. decomp t = send⟨[t]st#D"
by (metis (mono_tags, lifting) decomp_def prod.case surj_pair)

private lemma decomp_nonnil[simp]: "decomp t  []"
using decomp_snd_exists[of t] by fastforce

private lemma to_st_nil_inv[dest]: "to_st A = []  A = []"
by (induct A rule: to_st.induct) auto

private lemma well_analyzedD:
  assumes "well_analyzed A" "Decomp t  set A"
  shows "f T. t = Fun f T"
using assms
proof (induction A rule: well_analyzed.induct)
  case (Decomp A t')
  hence "f T. t' = Fun f T" by (cases t') auto
  moreover have "Decomp t  set A  t = t'" using Decomp by auto
  ultimately show ?case using Decomp.IH by auto
qed auto

private lemma well_analyzed_inv:
  assumes "well_analyzed (A@[Decomp t])"
  shows "t  subtermsset (ikest A  assignment_rhsest A) - (Var ` 𝒱)"
using assms well_analyzed.cases[of "A@[Decomp t]"] by fastforce

private lemma well_analyzed_split_left_single: "well_analyzed (A@[a])  well_analyzed A"
by (induction "A@[a]" rule: well_analyzed.induct) auto

private lemma well_analyzed_split_left: "well_analyzed (A@B)  well_analyzed A"
proof (induction B rule: List.rev_induct)
  case (snoc b B) thus ?case using well_analyzed_split_left_single[of "A@B" b] by simp
qed simp

private lemma well_analyzed_append:
  assumes "well_analyzed A" "well_analyzed B"
  shows "well_analyzed (A@B)"
using assms(2,1)
proof (induction B rule: well_analyzed.induct)
  case (Step B x) show ?case using well_analyzed.Step[OF Step.IH[OF Step.prems]] by simp
next
  case (Decomp B t) thus ?case
    using well_analyzed.Decomp[OF Decomp.IH[OF Decomp.prems]] ikest_append assignment_rhsest_append
    by auto
qed simp_all

private lemma well_analyzed_singleton:
  "well_analyzed [Step (send⟨tsst)]" "well_analyzed [Step (receive⟨tsst)]"
  "well_analyzed [Step (a: t  t'st)]" "well_analyzed [Step (X⟨∨≠: Fst)]"
  "¬well_analyzed [Decomp t]"
proof -
  show "well_analyzed [Step (send⟨tsst)]" "well_analyzed [Step (receive⟨tsst)]"
       "well_analyzed [Step (a: t  t'st)]" "well_analyzed [Step (X⟨∨≠: Fst)]"
    using well_analyzed.Step[OF well_analyzed.Nil]
    by simp_all

  show "¬well_analyzed [Decomp t]" using well_analyzed.cases[of "[Decomp t]"] by auto
qed

private lemma well_analyzed_decomp_rmest_fv: "well_analyzed A  fvest (decomp_rmest A) = fvest A"
proof
  assume "well_analyzed A" thus "fvest A  fvest (decomp_rmest A)"
  proof (induction A rule: well_analyzed.induct)
    case Decomp thus ?case using ik_assignment_rhs_decomp_fv decomp_rmest_append by auto
  next
    case (Step A x)
    have "fvest (A@[Step x]) = fvest A  fvstp x"
         "fvest (decomp_rmest (A@[Step x])) = fvest (decomp_rmest A)  fvstp x"
      using fvest_append decomp_rmest_append by auto
    thus ?case using Step by auto
  qed simp
qed (rule fv_decomp_rm)

private lemma semest_d_split_left: assumes "semest_d M0  (𝒜@𝒜')" shows "semest_d M0  𝒜"
using assms semest_d.cases by (induction 𝒜' rule: List.rev_induct) fastforce+

private lemma semest_d_eq_sem_st: "semest_d M0  𝒜 = M0; to_st 𝒜d' "
proof
  show "M0; to_st 𝒜d'   semest_d M0  𝒜"
  proof (induction 𝒜 arbitrary: M0 rule: List.rev_induct)
    case Nil show ?case using to_st_nil_inv by simp
  next
    case (snoc a 𝒜)
    hence IH: "semest_d M0  𝒜" and *: "ikest 𝒜  M0; to_st [a]d' "
      using to_st_append by (auto simp add: sup.commute)
    thus ?case using snoc
    proof (cases a)
      case (Step b) thus ?thesis
      proof (cases b)
        case (Send t) thus ?thesis using semest_d.Send[OF IH] * Step by auto
      next
        case (Receive t) thus ?thesis using semest_d.Receive[OF IH] Step by auto
      next
        case (Equality a t t') thus ?thesis using semest_d.Equality[OF IH] * Step by auto
      next
        case (Inequality X F) thus ?thesis using semest_d.Inequality[OF IH] * Step by auto
      qed
    next
      case (Decomp t)
      obtain K M where Ana: "Ana t = (K,M)" by atomize_elim auto
      have "to_st [a] = decomp t" using Decomp by auto
      hence "to_st [a] = [send⟨[t]st,Send K,Receive M]"
        using Ana unfolding decomp_def by auto
      hence **: "ikest 𝒜  M0 set   t  " and "ikest 𝒜  M0; [Send K]d' "
        using * by auto
      hence "k. k  set K  ikest 𝒜  M0 set   k  "
        using * strand_sem_Send_split(2) strand_sem_d.simps(2)
        unfolding strand_sem_eq_defs(2) list_all_iff
        by meson
      thus ?thesis using Decomp semest_d.Decompose[OF IH ** Ana] by metis
    qed
  qed

  show "semest_d M0  𝒜  M0; to_st 𝒜d' "
  proof (induction rule: semest_d.induct)
    case Nil thus ?case by simp
  next
    case (Send M0  𝒜 ts) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[send⟨tsst]"]
            to_st_append[of 𝒜 "[Step (send⟨tsst)]"]
      by (simp add: sup.commute)
  next
    case (Receive M0  𝒜 ts) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[receive⟨tsst]"]
            to_st_append[of 𝒜 "[Step (receive⟨tsst)]"]
      by (simp add: sup.commute)
  next
    case (Equality M0  𝒜 t t' a) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[a: t  t'st]"]
            to_st_append[of 𝒜 "[Step (a: t  t'st)]"]
      by (simp add: sup.commute)
  next
    case (Inequality M0  𝒜 X F) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[X⟨∨≠: Fst]"]
            to_st_append[of 𝒜 "[Step (X⟨∨≠: Fst)]"]
      by (simp add: sup.commute)
  next
    case (Decompose M0  𝒜 t K M)
    have "M0  ikst (to_st 𝒜); decomp td' "
    proof -
      have "M0  ikst (to_st 𝒜); [send⟨[t]st]d' "
        using Decompose.hyps(2) by (auto simp add: sup.commute)
      moreover have "k. k  set K  M0  ikst (to_st 𝒜) set   k  "
        using Decompose by (metis sup.commute)
      hence "k. k  set K  M0  ikst (to_st 𝒜); [Send1 k]d' " by auto
      hence "M0  ikst (to_st 𝒜); [Send K]d' "
        using strand_sem_Send_map(4)[of _ "M0  ikst (to_st 𝒜) set " ] strand_sem_Send_map(6)
        unfolding strand_sem_eq_defs(2) by auto
      moreover have "M0  ikst (to_st 𝒜); [Receive M]d' "
        by (metis strand_sem_Receive_map(6) strand_sem_eq_defs(2))
      ultimately have
          "M0  ikst (to_st 𝒜); [send⟨[t]st,send⟨Kst,receive⟨Mst]d' "
        by auto
      thus ?thesis using Decompose.hyps(3) unfolding decomp_def by auto
    qed
    hence "M0; to_st 𝒜@decomp td' "
      using strand_sem_append'[of M0 "to_st 𝒜"  "decomp t"] Decompose.IH
      by simp
    thus ?case using to_st_append[of 𝒜 "[Decomp t]"] by simp
  qed
qed

private lemma semest_c_eq_sem_st: "semest_c M0  𝒜 = M0; to_st 𝒜c' "
proof
  show "M0; to_st 𝒜c'   semest_c M0  𝒜"
  proof (induction 𝒜 arbitrary: M0 rule: List.rev_induct)
    case Nil show ?case using to_st_nil_inv by simp
  next
    case (snoc a 𝒜)
    hence IH: "semest_c M0  𝒜" and *: "ikest 𝒜  M0; to_st [a]c' "
      using to_st_append
      by (auto simp add: sup.commute)
    thus ?case using snoc
    proof (cases a)
      case (Step b) thus ?thesis
      proof (cases b)
        case (Send t) thus ?thesis using semest_c.Send[OF IH] * Step by auto
      next
        case (Receive t) thus ?thesis using semest_c.Receive[OF IH] Step by auto
      next
        case (Equality t) thus ?thesis using semest_c.Equality[OF IH] * Step by auto
      next
        case (Inequality t) thus ?thesis using semest_c.Inequality[OF IH] * Step by auto
      qed
    next
      case (Decomp t)
      obtain K M where Ana: "Ana t = (K,M)" by atomize_elim auto
      have "to_st [a] = decomp t" using Decomp by auto
      hence "to_st [a] = [send⟨[t]st,send⟨Kst,receive⟨Mst]"
        using Ana unfolding decomp_def by auto
      hence **: "ikest 𝒜  M0 set  c t  " and "ikest 𝒜  M0; [send⟨Kst]c' "
        using * by auto
      hence "ikest 𝒜  M0 set  c k  " when k: "k  set K" for k
        using * strand_sem_Send_split(5)[OF _ k] strand_sem_Send_map(5)
        unfolding strand_sem_eq_defs(1) by auto
      thus ?thesis using Decomp semest_c.Decompose[OF IH ** Ana] by metis
    qed
  qed

  show "semest_c M0  𝒜  M0; to_st 𝒜c' "
  proof (induction rule: semest_c.induct)
    case Nil thus ?case by simp
  next
    case (Send M0  𝒜 ts) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[send⟨tsst]"]
            to_st_append[of 𝒜 "[Step (send⟨tsst)]"]
      by (simp add: sup.commute)
  next
    case (Receive M0  𝒜 ts) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[receive⟨tsst]"]
            to_st_append[of 𝒜 "[Step (receive⟨tsst)]"]
      by (simp add: sup.commute)
  next
    case (Equality M0  𝒜 t t' a) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[a: t  t'st]"]
            to_st_append[of 𝒜 "[Step (a: t  t'st)]"]
      by (simp add: sup.commute)
  next
    case (Inequality M0  𝒜 X F) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜"  "[X⟨∨≠: Fst]"]
            to_st_append[of 𝒜 "[Step (X⟨∨≠: Fst)]"]
      by (auto simp add: sup.commute)
  next
    case (Decompose M0  𝒜 t K M)
    have "M0  ikst (to_st 𝒜); decomp tc' "
    proof -
      have "M0  ikst (to_st 𝒜); [send⟨[t]st]c' "
        using Decompose.hyps(2) by (auto simp add: sup.commute)
      moreover have "k. k  set K  M0  ikst (to_st 𝒜) set  c k  "
        using Decompose by (metis sup.commute)
      hence "k. k  set K  M0  ikst (to_st 𝒜); [Send1 k]c' " by auto
      hence "M0  ikst (to_st 𝒜); [Send K]c' "
        using strand_sem_Send_map(3)[of K, of "M0  ikst (to_st 𝒜) set " ]
              strand_sem_Send_map(5)
        unfolding strand_sem_eq_defs(1)
        by auto
      moreover have "M0  ikst (to_st 𝒜); [Receive M]c' "
        by (metis strand_sem_Receive_map(5) strand_sem_eq_defs(1))
      ultimately have
          "M0  ikst (to_st 𝒜); [send⟨[t]st,send⟨Kst,receive⟨Mst]c' "
        by auto
      thus ?thesis using Decompose.hyps(3) unfolding decomp_def by auto
    qed
    hence "M0; to_st 𝒜@decomp tc' "
      using strand_sem_append'[of M0 "to_st 𝒜"  "decomp t"] Decompose.IH
      by simp
    thus ?case using to_st_append[of 𝒜 "[Decomp t]"] by simp
  qed
qed

private lemma semest_c_decomp_rmest_deduct_aux:
  assumes "semest_c M0  A" "t  ikest A set " "t  ikest (decomp_rmest A) set "
  shows "ikest (decomp_rmest A)  M0 set   t"
using assms
proof (induction M0  A arbitrary: t rule: semest_c.induct)
  case (Send M0  A t') thus ?case using decomp_rmest_append ikest_append by auto
next
  case (Receive M0  A t')
  hence "t  ikest A set " "t  ikest (decomp_rmest A) set "
    using decomp_rmest_append ikest_append by auto
  hence IH: "ikest (decomp_rmest A)  M0 set   t" using Receive.IH by auto
  show ?case
    using ideduct_mono[OF IH] decomp_rmest_append ikest_append
    by (metis Un_subset_iff Un_upper1 Un_upper2 image_mono)
next
  case (Equality M0  A t') thus ?case using decomp_rmest_append ikest_append by auto
next
  case (Inequality M0  A t') thus ?case using decomp_rmest_append ikest_append by auto
next
  case (Decompose M0  A t' K M t)
  have *: "ikest (decomp_rmest A)  M0 set   t'  " using Decompose.hyps(2)
  proof (induction rule: intruder_synth_induct)
    case (AxiomC t'')
    moreover {
      assume "t''  ikest A set " "t''  ikest (decomp_rmest A) set "
      hence ?case using Decompose.IH by auto
    }
    ultimately show ?case by force
  qed simp
  
  { fix k assume "k  set K"
    hence "ikest A  M0 set  c k  " using Decompose.hyps by auto
    hence "ikest (decomp_rmest A)  M0 set   k  "
    proof (induction rule: intruder_synth_induct)
      case (AxiomC t'')
      moreover {
        assume "t''  ikest A set " "t''  ikest (decomp_rmest A) set "
        hence ?case using Decompose.IH by auto
      }
      ultimately show ?case by force
    qed simp
  }
  hence **: "k. k  set (K list )  ikest (decomp_rmest A)  M0 set   k" by auto
  
  show ?case
  proof (cases "t  ikest A set ")
    case True thus ?thesis using Decompose.IH Decompose.prems(2) decomp_rmest_append by auto
  next
    case False
    hence "t  ikst (decomp t') set " using Decompose.prems(1) ikest_append by auto
    hence ***: "t  set (M list )" using Decompose.hyps(3) decomp_ik by auto
    hence "M  []" by auto
    hence ****: "Ana (t'  ) = (K list , M list )" using Ana_subst[OF Decompose.hyps(3)] by auto

    have "ikest (decomp_rmest A)  M0 set   t" by (rule intruder_deduct.Decompose[OF * **** ** ***])
    thus ?thesis using ideduct_mono decomp_rmest_append by auto
  qed
qed simp

private lemma semest_c_decomp_rmest_deduct:
  assumes "semest_c M0  A" "ikest A  M0 set  c t"
  shows "ikest (decomp_rmest A)  M0 set   t"
using assms(2)
proof (induction t rule: intruder_synth_induct)
  case (AxiomC t)
  hence "t  ikest A set   t  M0 set " by auto
  moreover {
    assume "t  ikest A set " "t  ikest (decomp_rmest A) set "
    hence ?case using ideduct_mono[OF intruder_deduct.Axiom] by auto
  }
  moreover {
    assume "t  ikest A set " "t  ikest (decomp_rmest A) set "
    hence ?case using semest_c_decomp_rmest_deduct_aux[OF assms(1)] by auto
  }
  ultimately show ?case by auto
qed simp

private lemma semest_d_decomp_rmest_if_semest_c: "semest_c M0  A  semest_d M0  (decomp_rmest A)"
proof (induction M0  A rule: semest_c.induct)
  case (Send M0  A t)
  thus ?case
    using decomp_rmest_append semest_d.Send[OF Send.IH] semest_c_decomp_rmest_deduct
    unfolding list_all_iff by auto
next
  case (Receive t) thus ?case using decomp_rmest_append semest_d.Receive by auto
next
  case (Equality M0  A t)
  thus ?case
    using decomp_rmest_append semest_d.Equality[OF Equality.IH] semest_c_decomp_rmest_deduct
    by auto
next
  case (Inequality M0  A t)
  thus ?case
    using decomp_rmest_append semest_d.Inequality[OF Inequality.IH] semest_c_decomp_rmest_deduct
    by auto
next
  case Decompose thus ?case using decomp_rmest_append by auto
qed auto

private lemma semest_c_decompsest_append:
  assumes "semest_c {}  A" "D  decompsest (ikest A) (assignment_rhsest 𝒜) "
  shows "semest_c {}  (A@D)"
using assms(2,1)
proof (induction D rule: decompsest.induct)
  case (Decomp D f T K M)
  hence *: "semest_c {}  (A @ D)" "ikest (A@D)  {} set  c Fun f T  "
           "k. k  set K  ikest (A @ D)  {} set  c k  "
    using ikest_append by auto
  show ?case using semest_c.Decompose[OF *(1,2) Decomp.hyps(3) *(3)] by simp
qed auto

private lemma decompsest_preserves_wf:
  assumes "D  decompsest (ikest A) (assignment_rhsest A) " "wfest V A"
  shows "wfest V (A@D)"
using assms
proof (induction D rule: decompsest.induct)
  case (Decomp D f T K M)
  have "wfrestrictedvarsst (decomp (Fun f T))  fvset (ikest A  assignment_rhsest A)"
    using decomp_vars fv_subset_subterms[OF Decomp.hyps(2)] by fast
  hence "wfrestrictedvarsst (decomp (Fun f T))  wfrestrictedvarsest A"
    using ikst_assignment_rhsst_wfrestrictedvars_subset[of "to_st A"] by blast
  hence "wfrestrictedvarsst (decomp (Fun f T))  wfrestrictedvarsst (to_st (A@D))  V"
    using to_st_append[of A D] strand_vars_split(2)[of "to_st A" "to_st D"]
    by (metis le_supI1)
  thus ?case
    using wf_append_suffix[OF Decomp.IH[OF Decomp.prems], of "decomp (Fun f T)"]
          to_st_append[of "A@D" "[Decomp (Fun f T)]"]
    by auto
qed auto

private lemma decompsest_preserves_model_c:
  assumes "D  decompsest (ikest A) (assignment_rhsest A) " "semest_c M0  A"
  shows "semest_c M0  (A@D)"
using assms
proof (induction D rule: decompsest.induct)
  case (Decomp D f T K M) show ?case
    using semest_c.Decompose[OF Decomp.IH[OF Decomp.prems] _ Decomp.hyps(3)]
          Decomp.hyps(5,6) ideduct_synth_mono ikest_append
    by (metis (mono_tags, lifting) List.append_assoc image_Un sup_ge1) 
qed auto

private lemma decompsest_exist_aux:
  assumes "D  decompsest M N " "M  ikest D  t" "¬(M  (ikest D) c t)"
  obtains D' where
    "D@D'  decompsest M N " "M  ikest (D@D') c t" "M  ikest D  M  ikest (D@D')"
proof -
  have "D'  decompsest M N . M  ikest D' c t" using assms(2)
  proof (induction t rule: intruder_deduct_induct)
    case (Compose X f)
    from Compose.IH have "D  decompsest M N . x  set X. M  ikest D c x"
    proof (induction X)
      case (Cons t X)
      then obtain D' D'' where
          D': "D'  decompsest M N " "M  ikest D' c t" and
          D'': "D''  decompsest M N " "x  set X. M  ikest D'' c x"
        by atomize_elim force
      hence "M  ikest (D'@D'') c t" "x  set X. M  ikest (D'@D'') c x"
        by (auto intro: ideduct_synth_mono simp add: ikest_append)
      thus ?case using decompsest_append[OF D'(1) D''(1)] by (metis set_ConsD)
    qed (auto intro: decompsest.Nil)
    thus ?case using intruder_synth.ComposeC[OF Compose.hyps(1,2)] by metis
  next
    case (Decompose t K T ti)
    have "D  decompsest M N . k  set K. M  ikest D c k" using Decompose.IH
    proof (induction K)
      case (Cons t X)
      then obtain D' D'' where
          D': "D'  decompsest M N " "M  ikest D' c t" and
          D'': "D''  decompsest M N " "x  set X. M  ikest D'' c x"
        using assms(1) by atomize_elim force
      hence "M  ikest (D'@D'') c t" "x  set X. M  ikest (D'@D'') c x"
        by (auto intro: ideduct_synth_mono simp add: ikest_append)
      thus ?case using decompsest_append[OF D'(1) D''(1)] by auto
    qed auto
    then obtain D' where D': "D'  decompsest M N " "k. k  set K  M  ikest D' c k" by metis
    obtain D'' where D'': "D''  decompsest M N " "M  ikest D'' c t" by (metis Decompose.IH(1))
    obtain f X where fX: "t = Fun f X" "ti  set X"
      using Decompose.hyps(2,4) by (cases t) (auto dest: Ana_fun_subterm)
  
    from decompsest_append[OF D'(1) D''(1)] D'(2) D''(2) have *:
        "D'@D''  decompsest M N " "k. k  set K  M  ikest (D'@D'') c k"
        "M  ikest (D'@D'') c t"
      by (auto intro: ideduct_synth_mono simp add: ikest_append)
    hence **: "k. k  set K  M  ikest (D'@D'') set  c k  "
      using ideduct_synth_subst by auto

    have "ti  ikst (decomp t)" using Decompose.hyps(2,4) ik_rcv_map unfolding decomp_def by auto
    with *(3) fX(1) Decompose.hyps(2) show ?case
    proof (induction t rule: intruder_synth_induct)
      case (AxiomC t)
      hence t_in_subterms: "t  subtermsset (M  N)"
        using decompsest_ik_subset[OF *(1)] subset_subterms_Union
        by auto
      have "M  ikest (D'@D'') set  c t  "
        using ideduct_synth_subst[OF intruder_synth.AxiomC[OF AxiomC.hyps(1)]] by metis
      moreover have "T  []" using decomp_ik[OF Ana t = (K,T)] ti  ikst (decomp t) by auto
      ultimately have "D'@D''@[Decomp (Fun f X)]  decompsest M N "
        using AxiomC decompsest.Decomp[OF *(1) _ _ _ _ **] subset_subterms_Union t_in_subterms
        by (simp add: subset_eq)
      moreover have "decomp t = to_st [Decomp (Fun f X)]" using AxiomC.prems(1,2) by auto
      ultimately show ?case
        by (metis AxiomC.prems(3) UnCI intruder_synth.AxiomC ikest_append to_st_append)
    qed (auto intro!: fX(2) *(1))
  qed (fastforce intro: intruder_synth.AxiomC assms(1))
  hence "D'  decompsest M N . M  ikest (D@D') c t"
    by (auto intro: ideduct_synth_mono simp add: ikest_append)
  thus thesis using that[OF decompsest_append[OF assms(1)]] assms ikest_append by atomize_elim auto
qed

private lemma decompsest_ik_max_exist:
  assumes "finite A" "finite N"
  shows "D  decompsest A N . D'  decompsest A N . ikest D'  ikest D"
proof -
  let ?IK = "λM. D  M. ikest D"
  have "?IK (decompsest A N )  (t  A  N. subterms t)" by (auto dest!: decompsest_ik_subset)
  hence "finite (?IK (decompsest A N ))"
    using subterms_union_finite[OF assms(1)] subterms_union_finite[OF assms(2)] infinite_super
    by auto
  then obtain M where M: "finite M" "M  decompsest A N " "?IK M = ?IK (decompsest A N )"
    using finite_subset_Union by atomize_elim auto
  show ?thesis using decompsest_finite_ik_append[OF M(1,2)] M(3) by auto
qed

private lemma decompsest_exist:
  assumes "finite A" "finite N"
  shows "D  decompsest A N . t. A  t  A  ikest D c t"
proof (rule ccontr)
  assume neg: "¬(D  decompsest A N . t. A  t  A  ikest D c t)"

  obtain D where D: "D  decompsest A N " "D'  decompsest A N . ikest D'  ikest D"
    using decompsest_ik_max_exist[OF assms] by atomize_elim force
  then obtain t where t: "A  ikest D  t" "¬(A  ikest D c t)"
    using neg by (fastforce intro: ideduct_mono)

  obtain D' where D':
      "D@D'  decompsest A N " "A  ikest (D@D') c t"
      "A  ikest D  A  ikest (D@D')"
    by (metis decompsest_exist_aux t D(1))
  hence "ikest D  ikest (D@D')" using ikest_append by auto
  moreover have "ikest (D@D')  ikest D" using D(2) D'(1) by auto
  ultimately show False by simp
qed

private lemma decompsest_exist_subst:
  assumes "ikest A set   t  "
    and "semest_c {}  A" "wfest {} A" "interpretationsubst "
    and "Ana_invar_subst (ikest A  assignment_rhsest A)"
    and "well_analyzed A"
  shows "D  decompsest (ikest A) (assignment_rhsest A) . ikest (A@D) set  c t  "
proof -
  have ik_eq: "ikest (A est ) = ikest A set " using assms(5,6)
  proof (induction A rule: List.rev_induct)
    case (snoc a A)
    hence "Ana_invar_subst (ikest A  assignment_rhsest A)"
      using Ana_invar_subst_subset[OF snoc.prems(1)] ikest_append assignment_rhsest_append
      unfolding Ana_invar_subst_def by simp
    with snoc have IH:
        "ikest (A@[a] est ) = (ikest A set )  ikest ([a] est )"
        "ikest (A@[a]) set  = (ikest A set )  (ikest [a] set )"
      using well_analyzed_split_left[OF snoc.prems(2)]
      by (auto simp add: to_st_append ikest_append_subst)
      
    have "ikest [a estp ] = ikest [a] set "
    proof (cases a)
      case (Step b) thus ?thesis by (cases b) auto
    next
      case (Decomp t)
      then obtain f T where t: "t = Fun f T" using well_analyzedD[OF snoc.prems(2)] by force
      obtain K M where Ana_t: "Ana (Fun f T) = (K,M)" by (metis surj_pair)
      moreover have "Fun f T  subtermsset ((ikest (A@[a])  assignment_rhsest (A@[a])))"
        using t Decomp snoc.prems(2)
        by (auto dest: well_analyzed_inv simp add: ikest_append assignment_rhsest_append)
      hence "Ana (Fun f T  ) = (K list , M list )"
        using Ana_t snoc.prems(1) unfolding Ana_invar_subst_def by blast 
      ultimately show ?thesis using Decomp t by (auto simp add: decomp_ik)
    qed
    thus ?case using IH unfolding subst_apply_extstrand_def by simp
  qed simp
  moreover have assignment_rhs_eq: "assignment_rhsest (A est ) = assignment_rhsest A set "
    using assms(5,6)
  proof (induction A rule: List.rev_induct)
    case (snoc a A)
    hence "Ana_invar_subst (ikest A  assignment_rhsest A)"
      using Ana_invar_subst_subset[OF snoc.prems(1)] ikest_append assignment_rhsest_append
      unfolding Ana_invar_subst_def by simp
    hence "assignment_rhsest (A est ) = assignment_rhsest A set "
      using snoc.IH well_analyzed_split_left[OF snoc.prems(2)]
      by simp
    hence IH:
        "assignment_rhsest (A@[a] est ) = (assignment_rhsest A set )  assignment_rhsest ([a] est )"
        "assignment_rhsest (A@[a]) set  = (assignment_rhsest A set )  (assignment_rhsest [a] set )"
      by (metis assignment_rhsest_append_subst(1), metis assignment_rhsest_append_subst(2))

    have "assignment_rhsest [a estp ] = assignment_rhsest [a] set "
    proof (cases a)
      case (Step b) thus ?thesis by (cases b) auto
    next
      case (Decomp t)
      then obtain f T where t: "t = Fun f T" using well_analyzedD[OF snoc.prems(2)] by force
      obtain K M where Ana_t: "Ana (Fun f T) = (K,M)" by (metis surj_pair)
      moreover have "Fun f T  subtermsset ((ikest (A@[a])  assignment_rhsest (A@[a])))"
        using t Decomp snoc.prems(2)
        by (auto dest: well_analyzed_inv simp add: ikest_append assignment_rhsest_append)
      hence "Ana (Fun f T  ) = (K list , M list )"
        using Ana_t snoc.prems(1) unfolding Ana_invar_subst_def by blast
      ultimately show ?thesis using Decomp t by (auto simp add: decomp_assignment_rhs_empty)
    qed
    thus ?case using IH unfolding subst_apply_extstrand_def by simp
  qed simp
  ultimately obtain D where D:
      "D  decompsest (ikest A set ) (assignment_rhsest A set ) Var"
      "(ikest A set )  (ikest D) c t  "
    using decompsest_exist[OF ikest_finite assignment_rhsest_finite, of "A est " "A est "]
          ikest_append assignment_rhsest_append assms(1)
    by force

  let ?P = "λD D'. t. (ikest A set )  (ikest D) c t  (ikest A set )  (ikest D' set ) c t"

  have "D'  decompsest (ikest A) (assignment_rhsest A) . ?P D D'" using D(1)
  proof (induction D rule: decompsest.induct)
    case Nil
    have "ikest [] = ikest [] set " by auto
    thus ?case by (metis decompsest.Nil)
  next
    case (Decomp D f T K M)
    obtain D' where D': "D'  decompsest (ikest A) (assignment_rhsest A) " "?P D D'"
      using Decomp.IH by auto
    hence IH: "k. k  set K  (ikest A set )  (ikest D' set ) c k"
              "(ikest A set )  (ikest D' set ) c Fun f T"
      using Decomp.hyps(5,6) by auto

    have D'_ik: "ikest D' set   subtermsset ((ikest A  assignment_rhsest A)) set "
                "ikest D'  subtermsset (ikest A  assignment_rhsest A)"
      using decompsest_ik_subset[OF D'(1)] by (metis subst_all_mono, metis)

    show ?case using IH(2,1) Decomp.hyps(2,3,4)
    proof (induction "Fun f T" arbitrary: f T K M rule: intruder_synth_induct)
      case (AxiomC f T)
      then obtain s where s: "s  ikest A  ikest D'" "Fun f T = s  " using AxiomC.prems by blast
      hence fT_s_in: "Fun f T  (subtermsset (ikest A  assignment_rhsest A)) set "
                     "s  subtermsset (ikest A  assignment_rhsest A)"
        using AxiomC D'_ik subset_subterms_Union[of "ikest A  assignment_rhsest A"]
              subst_all_mono[OF subset_subterms_Union, of ]
        by (metis (no_types) Un_iff image_eqI subset_Un_eq, metis (no_types) Un_iff subset_Un_eq)
      obtain Ks Ms where Ana_s: "Ana s = (Ks,Ms)" by atomize_elim auto

      have AD'_props: "wfest {} (A@D')" "{}; to_st (A@D')c "
        using decompsest_preserves_model_c[OF D'(1) assms(2)]
              decompsest_preserves_wf[OF D'(1) assms(3)]
              semest_c_eq_sem_st strand_sem_eq_defs(1)
        by auto

      show ?case
      proof (cases s)
        case (Var x)
        ― ‹In this case ℐ x› (is a subterm of something that) was derived from an
            "earlier intruder knowledge" because A› is well-formed and has ℐ› as a model.
            So either the intruder composed Fun f T› himself (making Decomp (Fun f T)›
            unnecessary) or Fun f T› is an instance of something else in the intruder
            knowledge (in which case the "something" can be used in place of Fun f T›)›
        hence "Var x  ikest (A@D')" " x = Fun f T" using s ikest_append by auto

        show ?thesis
        proof (cases "m  set M. ikest A  ikest D' set  c m")
          case True
          ― ‹All terms acquired by decomposing Fun f T› are already derivable.
              Hence there is no need to consider decomposition of Fun f T› at all.›
          have *: "(ikest A set )  ikest (D@[Decomp (Fun f T)]) = (ikest A set )  ikest D  set M"
            using decomp_ik[OF Ana (Fun f T) = (K,M)] ikest_append[of D "[Decomp (Fun f T)]"]
            by auto
          
          { fix t' assume "(ikest A set )  ikest D  set M c t'"
            hence "(ikest A set )  (ikest D' set ) c t'"
            proof (induction t' rule: intruder_synth_induct)
              case (AxiomC t') thus ?case
              proof
                assume "t'  set M"
                moreover have "(ikest A set )  (ikest D' set ) = ikest A  ikest D' set " by auto
                ultimately show ?case using True by auto
              qed (metis D'(2) intruder_synth.AxiomC)
            qed auto
          }
          thus ?thesis using D'(1) * by metis
        next
          case False
          ― ‹Some term acquired by decomposition of Fun f T› cannot be derived in c.
              Fun f T› must therefore be an instance of something else in the intruder knowledge,
              because of well-formedness.›
          then obtain ti where ti: "ti  set T" "¬ikest (A@D') set  c ti"
            using Ana_fun_subterm[OF Ana (Fun f T) = (K,M)] by (auto simp add: ikest_append)
          obtain S where fS:
              "Fun f S  subtermsset (ikest (A@D')) 
               Fun f S  subtermsset (assignment_rhsest (A@D'))"
              " x = Fun f S  "
            using strand_sem_wf_ik_or_assignment_rhs_fun_subterm[
                    OF AD'_props Var x  ikest (A@D') _ ti interpretationsubst ]
                   x = Fun f T
            by atomize_elim metis
          hence fS_in: "Fun f S    ikest A  ikest D' set "
                       "Fun f S  subtermsset (ikest A  assignment_rhsest A)"
            using imageI[OF s(1), of "λx. x  "] Var
                  ikest_append[of A D'] assignment_rhsest_append[of A D']
                  decompsest_subterms[OF D'(1)] decompsest_assignment_rhs_empty[OF D'(1)]
            by auto
          obtain KS MS where Ana_fS: "Ana (Fun f S) = (KS, MS)" by atomize_elim auto
          hence "K = KS list " "M = MS list "
            using Ana_invar_substD[OF assms(5) fS_in(2)]
                  s(2) fS(2) s = Var x Ana (Fun f T) = (K,M)
            by simp_all
          hence "MS  []" using M  [] by simp
          have "k. k  set KS  ikest A  ikest D' set  c k  "
            using AxiomC.prems(1) K = KS list  by (simp add: image_Un)
          hence D'': "D'@[Decomp (Fun f S)]  decompsest (ikest A) (assignment_rhsest A) "
            using decompsest.Decomp[OF D'(1) fS_in(2) Ana_fS MS  []] AxiomC.prems(1)
                  intruder_synth.AxiomC[OF fS_in(1)]
            by simp
          moreover {
            fix t' assume "(ikest A set )  ikest (D@[Decomp (Fun f T)]) c t'"
            hence "(ikest A set )  (ikest (D'@[Decomp (Fun f S)]) set ) c t'"
            proof (induction t' rule: intruder_synth_induct)
              case (AxiomC t')
              hence "t'  (ikest A set )  ikest D  t'  ikest [Decomp (Fun f T)]"
                by (simp add: ikest_append)
              thus ?case
              proof
                assume "t'  ikest [Decomp (Fun f T)]"
                hence "t'  ikest [Decomp (Fun f S)] set "
                  using decomp_ik Ana (Fun f T) = (K,M) Ana (Fun f S) = (KS,MS) M = MS list 
                  by simp
                thus ?case
                  using ideduct_synth_mono[
                          OF intruder_synth.AxiomC[of t' "ikest [Decomp (Fun f S)] set "],
                          of "(ikest A set )  (ikest (D'@[Decomp (Fun f S)]) set )"]
                  by (auto simp add: ikest_append)
              next
                assume "t'  (ikest A set )  ikest D"
                hence "(ikest A set )  (ikest D' set ) c t'"
                  by (metis D'(2) intruder_synth.AxiomC)
                hence "(ikest A set )  (ikest D' set )  (ikest [Decomp (Fun f S)] set ) c t'"
                  by (simp add: ideduct_synth_mono)
                thus ?case
                  using ikest_append[of D' "[Decomp (Fun f S)]"]
                        image_Un[of "λx. x  " "ikest D'" "ikest [Decomp (Fun f S)]"]
                  by (simp add: sup_aci(2))
              qed
            qed auto
          }
          ultimately show ?thesis using D'' by auto
        qed
      next
        case (Fun g S) ― ‹Hence Decomp (Fun f T)› can be substituted for Decomp (Fun g S)›
        hence KM: "K = Ks list " "M = Ms list " "set K = set Ks set " "set M = set Ms set "
          using fT_s_in(2) Ana (Fun f T) = (K,M) Ana_s s(2)
                Ana_invar_substD[OF assms(5), of g S]
          by auto
        hence Ms_nonempty: "Ms  []" using M  [] by auto
        { fix t' assume "(ikest A set )  ikest (D@[Decomp (Fun f T)]) c t'"
          hence "(ikest A set )  (ikest (D'@[Decomp (Fun g S)]) set ) c t'" using AxiomC
          proof (induction t' rule: intruder_synth_induct)
            case (AxiomC t')
            hence "t'  ikest A set   t'  ikest D  t'  set M"
              by (simp add: decomp_ik ikest_append)
            thus ?case
            proof (elim disjE)
              assume "t'  ikest D"
              hence *: "(ikest A set )  (ikest D' set ) c t'" using D'(2) by simp
              show ?case by (auto intro: ideduct_synth_mono[OF *] simp add: ikest_append_subst(2))
            next
              assume "t'  set M"
              hence "t'  ikest [Decomp (Fun g S)] set "
                using KM(2) Fun decomp_ik[OF Ana_s] by auto
              thus ?case by (simp add: image_Un ikest_append)
            qed (simp add: ideduct_synth_mono[OF intruder_synth.AxiomC])
          qed auto
        }
        thus ?thesis
          using s Fun Ana_s AxiomC.prems(1) KM(3) fT_s_in
                decompsest.Decomp[OF D'(1) _ _ Ms_nonempty, of g S Ks]
          by (metis AxiomC.hyps image_Un image_eqI intruder_synth.AxiomC)
      qed
    next
      case (ComposeC T f)
      have *: "m. m  set M  (ikest A set )  (ikest D' set ) c m"
        using Ana_fun_subterm[OF Ana (Fun f T) = (K, M)] ComposeC.hyps(3)
        by auto
      
      have **: "ikest (D@[Decomp (Fun f T)]) = ikest D  set M"
        using decomp_ik[OF Ana (Fun f T) = (K, M)] ikest_append by auto

      { fix t' assume "(ikest A set )  ikest (D@[Decomp (Fun f T)]) c t'"
        hence "(ikest A set )  (ikest D' set ) c t'"
          by (induct rule: intruder_synth_induct) (auto simp add: D'(2) * **)
      }
      thus ?case using D'(1) by auto
    qed
  qed
  thus ?thesis using D(2) assms(1) by (auto simp add: ikest_append_subst(2))
qed

private lemma decompsest_exist_subst_list:
  assumes "t  set ts. ikest A set   t  "
    and "semest_c {}  A" "wfest {} A" "interpretationsubst "
    and "Ana_invar_subst (ikest A  assignment_rhsest A)"
    and "well_analyzed A"
  shows "D  decompsest (ikest A) (assignment_rhsest A) .
          t  set ts. ikest (A@D) set  c t  "
    (is "D  ?A. ?B D ts")
proof -
  note 0 = decompsest_exist_subst[OF _ assms(2-6)]

  show ?thesis using assms(1)
  proof (induction ts)
    case (Cons t ts)
    have 1: "ikest A set   t  " and 2: "t  set ts. ikest A set   t  "
      using Cons.prems by auto

    obtain D where D: "D  ?A" "ikest (A@D) set  c t  "
      using 0[OF 1] by blast

    obtain D' where D': "D'  ?A" "?B D' ts"
      using Cons.IH[OF 2] by auto

    have "ikest (A@D@D') set  c t  "
      using ideduct_synth_mono[OF D(2)] ikest_append_subst(2)[of  "A@D" D'] by fastforce
    hence "?B (D@D') (t#ts)"
      using D'(2) ideduct_synth_mono[of "ikest (A@D') set " _ "ikest (A@D@D') set "]
            ikest_append_subst(2)[of ]
      by auto
    thus ?case
      using decompsest_append[OF D(1) D'(1)] by blast
  qed (fastforce intro: decompsest.Nil)
qed

private lemma wfsts'_updatest_nil: assumes "wfsts' 𝒮 𝒜" shows "wfsts' (updatest 𝒮 []) 𝒜"
using assms unfolding wfsts'_def by auto

private lemma wfsts'_updatest_snd:
  assumes "wfsts' 𝒮 𝒜" "send⟨tsst#S  𝒮"
  shows "wfsts' (updatest 𝒮 (send⟨tsst#S)) (𝒜@[Step (receive⟨tsst)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "send⟨tsst#S"
  let ?A = "𝒜@[Step (receive⟨tsst)]"

  have 𝒮: "S'. S'  updatest 𝒮 ?S  S' = S  S'  𝒮" by auto

  have 1: "S  𝒮. wfst (wfrestrictedvarsest 𝒜) (dualst S)" using assms unfolding wfsts'_def by auto
  moreover have 2: "wfrestrictedvarsest ?A = wfrestrictedvarsest 𝒜  fvset (set ts)"
    using wfrestrictedvarsest_split(2) by (auto simp add: Un_assoc)
  ultimately have 3: "S  𝒮. wfst (wfrestrictedvarsest ?A) (dualst S)" by (metis wf_vars_mono)

  have 4: "S  𝒮. S'  𝒮. fvst S  bvarsst S' = {}" using assms unfolding wfsts'_def by simp

  have "wfst (wfrestrictedvarsest ?A) (dualst S)" using 1 2 3 assms(2) by auto
  thus "S  updatest 𝒮 ?S. wfst (wfrestrictedvarsest ?A) (dualst S)" by (metis 3 𝒮)
  
  have "fvst S  bvarsst S = {}"
       "S'  𝒮. fvst S  bvarsst S' = {}"
       "S'  𝒮. fvst S'  bvarsst S = {}"
    using 4 assms(2) unfolding wfsts'_def by force+
  thus "S  updatest 𝒮 ?S. S'  updatest 𝒮 ?S. fvst S  bvarsst S' = {}" by (metis 4 𝒮)

  have "S'  𝒮. fvst ?S  bvarsst S' = {}" "S'  𝒮. fvst S'  bvarsst ?S = {}"
    using assms unfolding wfsts'_def by metis+
  hence 5: "fvest ?A = fvest 𝒜  fvset (set ts)" "bvarsest ?A = bvarsest 𝒜"
           "S'  𝒮. fvset (set ts)  bvarsst S' = {}"
    using to_st_append by fastforce+

  have *: "S  𝒮. fvst S  bvarsest ?A = {}"
    using 5 assms(1) unfolding wfsts'_def by fast
  hence "fvst ?S  bvarsest ?A = {}" using assms(2) by metis
  hence "fvst S  bvarsest ?A = {}" by auto
  thus "S  updatest 𝒮 ?S. fvst S  bvarsest ?A = {}" by (metis * 𝒮)

  have **: "S  𝒮. fvest ?A  bvarsst S = {}"
    using 5 assms(1) unfolding wfsts'_def by fast
  hence "fvest ?A  bvarsst ?S = {}" using assms(2) by metis
  hence "fvest ?A  bvarsst S = {}" by fastforce
  thus "S  updatest 𝒮 ?S. fvest ?A  bvarsst S = {}" by (metis ** 𝒮)
qed

private lemma wfsts'_updatest_rcv:
  assumes "wfsts' 𝒮 𝒜" "receive⟨tsst#S  𝒮"
  shows "wfsts' (updatest 𝒮 (receive⟨tsst#S)) (𝒜@[Step (send⟨tsst)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "receive⟨tsst#S"
  let ?A = "𝒜@[Step (send⟨tsst)]"

  have 𝒮: "S'. S'  updatest 𝒮 ?S  S' = S  S'  𝒮" by auto

  have 1: "S  𝒮. wfst (wfrestrictedvarsest 𝒜) (dualst S)" using assms unfolding wfsts'_def by auto
  moreover have 2: "wfrestrictedvarsest ?A = wfrestrictedvarsest 𝒜  fvset (set ts)"
    using wfrestrictedvarsest_split(2) by (auto simp add: Un_assoc)
  ultimately have 3: "S  𝒮. wfst (wfrestrictedvarsest ?A) (dualst S)" by (metis wf_vars_mono)

  have 4: "S  𝒮. S'  𝒮. fvst S  bvarsst S' = {}" using assms unfolding wfsts'_def by simp

  have "wfst (wfrestrictedvarsest ?A) (dualst S)" using 1 2 3 assms(2) by auto
  thus "S  updatest 𝒮 ?S. wfst (wfrestrictedvarsest ?A) (dualst S)" by (metis 3 𝒮)

  have "fvst S  bvarsst S = {}"
       "S'  𝒮. fvst S  bvarsst S' = {}"
       "S'  𝒮. fvst S'  bvarsst S = {}"
    using 4 assms(2) unfolding wfsts'_def by force+
  thus "S  updatest 𝒮 ?S. S'  updatest 𝒮 ?S. fvst S  bvarsst S' = {}" by (metis 4 𝒮)

  have "S'  𝒮. fvst ?S  bvarsst S' = {}" "S'  𝒮. fvst S'  bvarsst ?S = {}"
    using assms unfolding wfsts'_def by metis+
  hence 5: "fvest ?A = fvest 𝒜  fvset (set ts)" "bvarsest ?A = bvarsest 𝒜"
            "S'  𝒮. fvset (set ts)  bvarsst S' = {}"
    using to_st_append by fastforce+

  have *: "S  𝒮. fvst S  bvarsest ?A = {}"
    using 5 assms(1) unfolding wfsts'_def by fast
  hence "fvst ?S  bvarsest ?A = {}" using assms(2) by metis
  hence "fvst S  bvarsest ?A = {}" by auto
  thus "S  updatest 𝒮 ?S. fvst S  bvarsest ?A = {}" by (metis * 𝒮)

  have **: "S  𝒮. fvest ?A  bvarsst S = {}"
    using 5 assms(1) unfolding wfsts'_def by fast
  hence "fvest ?A  bvarsst ?S = {}" using assms(2) by metis
  hence "fvest ?A  bvarsst S = {}" by fastforce
  thus "S  updatest 𝒮 ?S. fvest ?A  bvarsst S = {}" by (metis ** 𝒮)
qed

private lemma wfsts'_updatest_eq:
  assumes "wfsts' 𝒮 𝒜" "a: t  t'st#S  𝒮"
  shows "wfsts' (updatest 𝒮 (a: t  t'st#S)) (𝒜@[Step (a: t  t'st)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "a: t  t'st#S"
  let ?A = "𝒜@[Step (a: t  t'st)]"

  have 𝒮: "S'. S'  updatest 𝒮 ?S  S' = S  S'  𝒮" by auto

  have 1: "S  𝒮. wfst (wfrestrictedvarsest 𝒜) (dualst S)" using assms unfolding wfsts'_def by auto
  moreover have 2:
      "a = Assign  wfrestrictedvarsest ?A = wfrestrictedvarsest 𝒜  fv t  fv t'"
      "a = Check  wfrestrictedvarsest ?A = wfrestrictedvarsest 𝒜"
    using wfrestrictedvarsest_split(2) by (auto simp add: Un_assoc)
  ultimately have 3: "S  𝒮. wfst (wfrestrictedvarsest ?A) (dualst S)"
    by (cases a) (metis wf_vars_mono, metis)

  have 4: "S  𝒮. S'  𝒮. fvst S  bvarsst S' = {}" using assms unfolding wfsts'_def by simp

  have "wfst (wfrestrictedvarsest ?A) (dualst S)" using 1 2 3 assms(2) by (cases a) auto
  thus "S  updatest 𝒮 ?S. wfst (wfrestrictedvarsest ?A) (dualst S)" by (metis 3 𝒮)

  have "fvst S  bvarsst S = {}"
       "S'  𝒮. fvst S  bvarsst S' = {}"
       "S'  𝒮. fvst S'  bvarsst S = {}"
    using 4 assms(2) unfolding wfsts'_def by force+
  thus "S  updatest 𝒮 ?S. S'  updatest 𝒮 ?S. fvst S  bvarsst S' = {}" by (metis 4 𝒮)

  have "S'  𝒮. fvst ?S  bvarsst S' = {}" "S'  𝒮. fvst S'  bvarsst ?S = {}"
    using assms unfolding wfsts'_def by metis+
  hence 5: "fvest ?A = fvest 𝒜  fv t  fv t'" "bvarsest ?A = bvarsest 𝒜"
           "S'  𝒮. fv t  bvarsst S' = {}" "S'  𝒮. fv t'  bvarsst S' = {}"
    using to_st_append by fastforce+

  have *: "S  𝒮. fvst S  bvarsest ?A = {}"
    using 5 assms(1) unfolding wfsts'_def by fast
  hence "fvst ?S  bvarsest ?A = {}" using assms(2) by metis
  hence "fvst S  bvarsest ?A = {}" by auto
  thus "S  updatest 𝒮 ?S. fvst S  bvarsest ?A = {}" by (metis * 𝒮)

  have **: "S  𝒮. fvest ?A  bvarsst S = {}"
    using 5 assms(1) unfolding wfsts'_def by fast
  hence "fvest ?A  bvarsst ?S = {}" using assms(2) by metis
  hence "fvest ?A  bvarsst S = {}" by fastforce
  thus "S  updatest 𝒮 ?S. fvest ?A  bvarsst S = {}" by (metis ** 𝒮)
qed

private lemma wfsts'_updatest_ineq:
  assumes "wfsts' 𝒮 𝒜" "X⟨∨≠: Fst#S  𝒮"
  shows "wfsts' (updatest 𝒮 (X⟨∨≠: Fst#S)) (𝒜@[Step (X⟨∨≠: Fst)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "X⟨∨≠: Fst#S"
  let ?A = "𝒜@[Step (X⟨∨≠: Fst)]"

  have 𝒮: "S'. S'  updatest 𝒮 ?S  S' = S  S'  𝒮" by auto

  have 1: "S  𝒮. wfst (wfrestrictedvarsest 𝒜) (dualst S)" using assms unfolding wfsts'_def by auto
  moreover have 2: "wfrestrictedvarsest ?A = wfrestrictedvarsest 𝒜"
    using wfrestrictedvarsest_split(2) by (auto simp add: Un_assoc)
  ultimately have 3: "S  𝒮. wfst (wfrestrictedvarsest ?A) (dualst S)" by metis

  have 4: "S  𝒮. S'  𝒮. fvst S  bvarsst S' = {}" using assms unfolding wfsts'_def by simp

  have "wfst (wfrestrictedvarsest ?A) (dualst S)" using 1 2 3 assms(2) by auto
  thus "S  updatest 𝒮 ?S. wfst (wfrestrictedvarsest ?A) (dualst S)" by (metis 3 𝒮)

  have "fvst S  bvarsst S = {}"
       "S'  𝒮. fvst S  bvarsst S' = {}"
       "S'  𝒮. fvst S'  bvarsst S = {}"
    using 4 assms(2) unfolding wfsts'_def by force+
  thus "S  updatest 𝒮 ?S. S'  updatest 𝒮 ?S. fvst S  bvarsst S' = {}" by (metis 4 𝒮)

  have "S'  𝒮. fvst ?S  bvarsst S' = {}" "S'  𝒮. fvst S'  bvarsst ?S = {}"
    using assms unfolding wfsts'_def by metis+
  moreover have "fvpairs F - set X  fvst (X⟨∨≠: Fst # S)" by auto
  ultimately have 5:
      "S'  𝒮. (fvpairs F - set X)  bvarsst S' = {}"
      "fvest ?A = fvest 𝒜  (fvpairs F - set X)" "bvarsest ?A = set X  bvarsest 𝒜" 
      "S  𝒮. fvst S  set X = {}"
    using to_st_append
    by (blast, force, force, force)

  have *: "S  𝒮. fvst S  bvarsest ?A = {}" using 5(3,4) assms(1) unfolding wfsts'_def by blast
  hence "fvst ?S  bvarsest ?A = {}" using assms(2) by metis
  hence "fvst S  bvarsest ?A = {}" by auto
  thus "S  updatest 𝒮 ?S. fvst S  bvarsest ?A = {}" by (metis * 𝒮)

  have **: "S  𝒮. fvest ?A  bvarsst S = {}"
    using 5(1,2) assms(1) unfolding wfsts'_def by fast
  hence "fvest ?A  bvarsst ?S = {}" using assms(2) by metis
  hence "fvest ?A  bvarsst S = {}" by auto
  thus "S  updatest 𝒮 ?S. fvest ?A  bvarsst S = {}" by (metis ** 𝒮)
qed

private lemma trmsst_updatest_eq:
  assumes "x#S  𝒮"
  shows "(trmsst ` updatest 𝒮 (x#S))  trmsstp x = (trmsst ` 𝒮)" (is "?A = ?B")
proof
  show "?B  ?A"
  proof
    have "trmsstp x  trmsst (x#S)" by auto
    hence "t'. t'  ?B  t'  trmsstp x  t'  ?A" by simp
    moreover {
      fix t' assume t': "t'  ?B" "t'  trmsstp x"
      then obtain S' where S': "t'  trmsst S'" "S'  𝒮" by auto
      hence "S' = x#S  S'  updatest 𝒮 (x#S)" by auto
      moreover {
        assume "S' = x#S"
        hence "t'  trmsst S" using S' t' by simp
        hence "t'  ?A" by auto
      }
      ultimately have "t'  ?A" using t' S' by auto
    }
    ultimately show "t'. t'  ?B  t'  ?A" by metis
  qed

  show "?A  ?B"
  proof
    have "t'. t'  ?A  t'  trmsstp x  trmsstp x  ?B"
      using assms by force+
    moreover {
      fix t' assume t': "t'  ?A" "t'  trmsstp x"
      then obtain S' where "t'  trmsst S'" "S'  updatest 𝒮 (x#S)" by auto
      hence "S' = S  S'  𝒮" by auto
      moreover have "trmsst S  ?B" using assms trmsst_cons[of x S] by blast
      ultimately have "t'  ?B" using t' by fastforce
    }
    ultimately show "t'. t'  ?A  t'  ?B" by blast
  qed
qed

private lemma trmsst_updatest_eq_snd:
  assumes "send⟨tsst#S  𝒮" "𝒮' = updatest 𝒮 (send⟨tsst#S)" "𝒜' = 𝒜@[Step (receive⟨tsst)]"
  shows "((trmsst ` 𝒮))  (trmsest 𝒜) = ((trmsst ` 𝒮'))  (trmsest 𝒜')"
proof -
  have "(trmsest 𝒜') = (trmsest 𝒜)  set ts" "(trmsst ` 𝒮')  set ts = (trmsst ` 𝒮)"
    using to_st_append trmsst_updatest_eq[OF assms(1)] assms(2,3) by auto
  thus ?thesis
    by (metis (no_types, lifting) Un_commute Un_left_commute)
qed

private lemma trmsst_updatest_eq_rcv:
  assumes "receive⟨tsst#S  𝒮" "𝒮' = updatest 𝒮 (receive⟨tsst#S)" "𝒜' = 𝒜@[Step (send⟨tsst)]"
  shows "((trmsst ` 𝒮))  (trmsest 𝒜) = ((trmsst ` 𝒮'))  (trmsest 𝒜')"
proof -
  have "(trmsest 𝒜') = (trmsest 𝒜)  set ts" "(trmsst ` 𝒮')  set ts = (trmsst ` 𝒮)"
    using to_st_append trmsst_updatest_eq[OF assms(1)] assms(2,3) by auto
  thus ?thesis
    by (metis (no_types, lifting) Un_commute Un_left_commute)
qed

private lemma trmsst_updatest_eq_eq:
  assumes "a: t  t'st#S  𝒮" "𝒮' = updatest 𝒮 (a: t  t'st#S)" "𝒜' = 𝒜@[Step (a: t  t'st)]"
  shows "((trmsst ` 𝒮))  (trmsest 𝒜) = ((trmsst ` 𝒮'))  (trmsest 𝒜')"
proof -
  have "(trmsest 𝒜') = (trmsest 𝒜)  {t,t'}" "(trmsst ` 𝒮')  {t,t'} = (trmsst ` 𝒮)"
    using to_st_append trmsst_updatest_eq[OF assms(1)] assms(2,3) by auto
  thus ?thesis
    by (metis (no_types, lifting) Un_insert_left Un_insert_right sup_bot.right_neutral)
qed

private lemma trmsst_updatest_eq_ineq:
  assumes "X⟨∨≠: Fst#S  𝒮" "𝒮' = updatest 𝒮 (X⟨∨≠: Fst#S)" "𝒜' = 𝒜@[Step (X⟨∨≠: Fst)]"
  shows "((trmsst ` 𝒮))  (trmsest 𝒜) = ((trmsst ` 𝒮'))  (trmsest 𝒜')"
proof -
  have "(trmsest 𝒜') = (trmsest 𝒜)  trmspairs F" "(trmsst ` 𝒮')  trmspairs F = (trmsst ` 𝒮)"
    using to_st_append trmsst_updatest_eq[OF assms(1)] assms(2,3) by auto
  thus ?thesis by (simp add: Un_commute sup_left_commute)
qed

private lemma ikst_updatest_subset:
  assumes "x#S  𝒮"
  shows "(ikst`dualst ` (updatest 𝒮 (x#S)))  (ikst`dualst ` 𝒮)" (is ?A)
        "(assignment_rhsst ` (updatest 𝒮 (x#S)))  (assignment_rhsst ` 𝒮)" (is ?B)
proof -
  { fix t assume "t  (ikst`dualst ` (updatest 𝒮 (x#S)))"
    then obtain S' where S': "S'  updatest 𝒮 (x#S)" "t  ikst (dualst S')" by auto
  
    have *: "ikst (dualst S)  ikst (dualst (x#S))"
      using ik_append[of "dualst [x]" "dualst S"] dualst_append[of "[x]" S]
      by auto
  
    hence "t  (ikst`dualst ` 𝒮)"
    proof (cases "S' = S")
      case True thus ?thesis using * assms S' by auto
    next
      case False thus ?thesis using S' by auto
    qed
  }
  moreover
  { fix t assume "t  (assignment_rhsst ` (updatest 𝒮 (x#S)))"
    then obtain S' where S': "S'  updatest 𝒮 (x#S)" "t  assignment_rhsst S'" by auto
  
    have "assignment_rhsst S  assignment_rhsst (x#S)"
      using assignment_rhs_append[of "[x]" S] by simp
    hence "t  (assignment_rhsst ` 𝒮)"
      using assms S' by (cases "S' = S") auto
  }
  ultimately show ?A ?B by (metis subsetI)+
qed

private lemma ikst_updatest_subset_snd:
  assumes "send⟨tsst#S  𝒮"
          "𝒮' = updatest 𝒮 (send⟨tsst#S)"
          "𝒜' = 𝒜@[Step (receive⟨tsst)]"
  shows "((ikst ` dualst ` 𝒮'))  (ikest 𝒜') 
         ((ikst ` dualst ` 𝒮))  (ikest 𝒜)" (is ?A)
        "((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜') 
         ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)" (is ?B)
proof -
  { fix t' assume t'_in: "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜')"
    hence "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜)  set ts" using assms ikest_append by auto
    moreover have "set ts  (ikst`dualst ` 𝒮)" using assms(1) by force
    ultimately have "t'  ((ikst`dualst ` 𝒮))  (ikest 𝒜)"
      using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  }
  moreover
  { fix t' assume t'_in: "t'  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜')"
    hence "t'  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜)"
      using assms assignment_rhsest_append by auto
    hence "t'  ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)"
      using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  }
  ultimately show ?A ?B by (metis subsetI)+
qed

private lemma ikst_updatest_subset_rcv:
  assumes "receive⟨tst#S  𝒮"
          "𝒮' = updatest 𝒮 (receive⟨tst#S)"
          "𝒜' = 𝒜@[Step (send⟨tst)]"
  shows "((ikst ` dualst ` 𝒮'))  (ikest 𝒜') 
         ((ikst ` dualst ` 𝒮))  (ikest 𝒜)" (is ?A)
        "((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜') 
         ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)" (is ?B)
proof -
  { fix t' assume t'_in: "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜')"
    hence "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜)" using assms ikest_append by auto
    hence "t'  ((ikst`dualst ` 𝒮))  (ikest 𝒜)"
      using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  }
  moreover
  { fix t' assume t'_in: "t'  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜')"
    hence "t'  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜)"
      using assms assignment_rhsest_append by auto
    hence "t'  ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)"
      using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  }
  ultimately show ?A ?B by (metis subsetI)+
qed

private lemma ikst_updatest_subset_eq:
  assumes "a: t  t'st#S  𝒮"
          "𝒮' = updatest 𝒮 (a: t  t'st#S)"
          "𝒜' = 𝒜@[Step (a: t  t'st)]"
  shows "((ikst ` dualst ` 𝒮'))  (ikest 𝒜') 
         ((ikst ` dualst ` 𝒮))  (ikest 𝒜)" (is ?A)
        "((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜') 
         ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)" (is ?B)
proof -
  have 1: "t'  ((ikst`dualst ` 𝒮))  (ikest 𝒜)"
    when "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜')"
    for t'
  proof -
    have "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜)" using that assms ikest_append by auto
    thus ?thesis using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  qed

  have 2: "t''  ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)"
    when "t''  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜')" "a = Assign"
    for t''
  proof -
    have "t''  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜)  {t'}"
      using that assms assignment_rhsest_append by auto
    moreover have "t'  (assignment_rhsst ` 𝒮)" using assms(1) that by force
    ultimately show ?thesis using ikst_updatest_subset[OF assms(1)] assms(2) that by auto
  qed

  have 3: "assignment_rhsest 𝒜' = assignment_rhsest 𝒜" (is ?C)
          "((assignment_rhsst ` 𝒮'))  ((assignment_rhsst ` 𝒮))" (is ?D)
    when "a = Check"
  proof -
    show ?C using that assms(2,3) by (simp add: assignment_rhsest_append)
    show ?D using assms(1,2,3) ikst_updatest_subset(2) by auto 
  qed

  show ?A using 1 2 by (metis subsetI)
  show ?B using 1 2 3 by (cases a) blast+
qed

private lemma ikst_updatest_subset_ineq:
  assumes "X⟨∨≠: Fst#S  𝒮"
          "𝒮' = updatest 𝒮 (X⟨∨≠: Fst#S)"
          "𝒜' = 𝒜@[Step (X⟨∨≠: Fst)]"
  shows "((ikst`dualst ` 𝒮'))  (ikest 𝒜') 
          ((ikst`dualst ` 𝒮))  (ikest 𝒜)" (is ?A)
        "((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜') 
         ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)" (is ?B)
proof -
  { fix t' assume t'_in: "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜')"
    hence "t'  ((ikst`dualst ` 𝒮'))  (ikest 𝒜)" using assms ikest_append by auto
    hence "t'  ((ikst`dualst ` 𝒮))  (ikest 𝒜)"
      using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  }
  moreover
  { fix t' assume t'_in: "t'  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜')"
    hence "t'  ((assignment_rhsst ` 𝒮'))  (assignment_rhsest 𝒜)"
      using assms assignment_rhsest_append by auto
    hence "t'  ((assignment_rhsst ` 𝒮))  (assignment_rhsest 𝒜)"
      using ikst_updatest_subset[OF assms(1)] assms(2) by auto
  }
  ultimately show ?A ?B by (metis subsetI)+
qed


subsubsection ‹Transition Systems Definitions›
inductive pts_symbolic::
  "(('fun,'var) strands × ('fun,'var) strand) 
   (('fun,'var) strands × ('fun,'var) strand)  bool"
(infix "" 50) where
  Nil[simp]:        "[]  𝒮  (𝒮,𝒜)  (updatest 𝒮 [],𝒜)"
| Send[simp]:       "send⟨tst#S  𝒮  (𝒮,𝒜)  (updatest 𝒮 (send⟨tst#S),𝒜@[receive⟨tst])"
| Receive[simp]:    "receive⟨tst#S  𝒮  (𝒮,𝒜)  (updatest 𝒮 (receive⟨tst#S),𝒜@[send⟨tst])"
| Equality[simp]:   "a: t  t'st#S  𝒮  (𝒮,𝒜)  (updatest 𝒮 (a: t  t'st#S),𝒜@[a: t  t'st])"
| Inequality[simp]: "X⟨∨≠: Fst#S  𝒮  (𝒮,𝒜)  (updatest 𝒮 (X⟨∨≠: Fst#S),𝒜@[X⟨∨≠: Fst])"

private inductive pts_symbolic_c::
  "(('fun,'var) strands × ('fun,'var) extstrand) 
   (('fun,'var) strands × ('fun,'var) extstrand)  bool"
(infix "c" 50) where
  Nil[simp]:        "[]  𝒮  (𝒮,𝒜) c (updatest 𝒮 [],𝒜)"
| Send[simp]:       "send⟨tst#S  𝒮  (𝒮,𝒜) c (updatest 𝒮 (send⟨tst#S),𝒜@[Step (receive⟨tst)])"
| Receive[simp]:    "receive⟨tst#S  𝒮  (𝒮,𝒜) c (updatest 𝒮 (receive⟨tst#S),𝒜@[Step (send⟨tst)])"
| Equality[simp]:   "a: t  t'st#S  𝒮  (𝒮,𝒜) c (updatest 𝒮 (a: t  t'st#S),𝒜@[Step (a: t  t'st)])"
| Inequality[simp]: "X⟨∨≠: Fst#S  𝒮  (𝒮,𝒜) c (updatest 𝒮 (X⟨∨≠: Fst#S),𝒜@[Step (X⟨∨≠: Fst)])"
| Decompose[simp]:  "Fun f T  subtermsset (ikest 𝒜  assignment_rhsest 𝒜)
                      (𝒮,𝒜) c (𝒮,𝒜@[Decomp (Fun f T)])"

abbreviation pts_symbolic_rtrancl (infix "*" 50) where "a * b  pts_symbolic** a b"
private abbreviation pts_symbolic_c_rtrancl (infix "c*" 50) where "a c* b  pts_symbolic_c** a b"

lemma pts_symbolic_induct[consumes 1, case_names Nil Send Receive Equality Inequality]:
  assumes "(𝒮,𝒜)  (𝒮',𝒜')"
  and "[]  𝒮; 𝒮' = updatest 𝒮 []; 𝒜' = 𝒜  P"
  and "t S. send⟨tst#S  𝒮; 𝒮' = updatest 𝒮 (send⟨tst#S); 𝒜' = 𝒜@[receive⟨tst]  P"
  and "t S. receive⟨tst#S  𝒮; 𝒮' = updatest 𝒮 (receive⟨tst#S); 𝒜' = 𝒜@[send⟨tst]  P"
  and "a t t' S. a: t  t'st#S  𝒮; 𝒮' = updatest 𝒮 (a: t  t'st#S); 𝒜' = 𝒜@[a: t  t'st]  P"
  and "X F S. X⟨∨≠: Fst#S  𝒮; 𝒮' = updatest 𝒮 (X⟨∨≠: Fst#S); 𝒜' = 𝒜@[X⟨∨≠: Fst]  P"
  shows "P"
apply (rule pts_symbolic.cases[OF assms(1)])
using assms(2,3,4,5,6) by simp_all

private lemma pts_symbolic_c_induct[consumes 1, case_names Nil Send Receive Equality Inequality Decompose]:
  assumes "(𝒮,𝒜) c (𝒮',𝒜')"
  and "[]  𝒮; 𝒮' = updatest 𝒮 []; 𝒜' = 𝒜  P"
  and "t S. send⟨tst#S  𝒮; 𝒮' = updatest 𝒮 (send⟨tst#S); 𝒜' = 𝒜@[Step (receive⟨tst)]  P"
  and "t S. receive⟨tst#S  𝒮; 𝒮' = updatest 𝒮 (receive⟨tst#S); 𝒜' = 𝒜@[Step (send⟨tst)]  P"
  and "a t t' S. a: t  t'st#S  𝒮; 𝒮' = updatest 𝒮 (a: t  t'st#S); 𝒜' = 𝒜@[Step (a: t  t'st)]  P"
  and "X F S. X⟨∨≠: Fst#S  𝒮; 𝒮' = updatest 𝒮 (X⟨∨≠: Fst#S); 𝒜' = 𝒜@[Step (X⟨∨≠: Fst)]  P"
  and "f T. Fun f T  subtermsset (ikest 𝒜  assignment_rhsest 𝒜); 𝒮' = 𝒮; 𝒜' = 𝒜@[Decomp (Fun f T)]  P"
  shows "P"
apply (rule pts_symbolic_c.cases[OF assms(1)])
using assms(2,3,4,5,6,7) by simp_all

private lemma pts_symbolic_c_preserves_wf_prot:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')" "wfsts' 𝒮 𝒜"
  shows "wfsts' 𝒮' 𝒜'"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  from step.hyps(2) step.IH[OF step.prems] show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Decompose
    hence "fvest 𝒜2 = fvest 𝒜1" "bvarsest 𝒜2 = bvarsest 𝒜1"
      using bvars_decomp ik_assignment_rhs_decomp_fv by metis+
    thus ?case using Decompose unfolding wfsts'_def
      by (metis wf_vars_mono wfrestrictedvarsest_split(2))
  qed (metis wfsts'_updatest_nil, metis wfsts'_updatest_snd,
       metis wfsts'_updatest_rcv, metis wfsts'_updatest_eq,
       metis wfsts'_updatest_ineq)
qed metis

private lemma pts_symbolic_c_preserves_wf_is:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')" "wfsts' 𝒮 𝒜" "wfst V (to_st 𝒜)"
  shows "wfst V (to_st 𝒜')"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  hence "(𝒮, 𝒜) c* (𝒮2, 𝒜2)" by auto
  hence *: "wfsts' 𝒮1 𝒜1" "wfsts' 𝒮2 𝒜2"
    using pts_symbolic_c_preserves_wf_prot[OF _ step.prems(1)] step.hyps(1)
    by auto

  from step.hyps(2) step.IH[OF step.prems] show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Nil thus ?case by auto
  next
    case (Send ts S)
    hence "wfst (wfrestrictedvarsest 𝒜1) (receive⟨tsst#(dualst S))"
      using *(1) unfolding wfsts'_def by fastforce
    hence "fvset (set ts)  wfrestrictedvarsst (to_st 𝒜1)  V"
      using wfrestrictedvarsest_eq_wfrestrictedvarsst by auto
    thus ?case using Send wf_rcv_append''' to_st_append by simp
  next
    case (Receive ts) thus ?case using wf_snd_append to_st_append by simp
  next
    case (Equality a t t' S)
    hence "wfst (wfrestrictedvarsest 𝒜1) (a: t  t'st#(dualst S))"
      using *(1) unfolding wfsts'_def by fastforce
    hence "fv t'  wfrestrictedvarsst (to_st 𝒜1)  V" when "a = Assign"
      using wfrestrictedvarsest_eq_wfrestrictedvarsst that by auto
    thus ?case using Equality wf_eq_append''' to_st_append by (cases a) auto
  next
    case (Inequality t t' S) thus ?case using wf_ineq_append'' to_st_append by simp
  next
    case (Decompose f T)
    hence "fv (Fun f T)  wfrestrictedvarsest 𝒜1"
      by (metis fv_subterms_set fv_subset subset_trans
                ikst_assignment_rhsst_wfrestrictedvars_subset)
    hence "varsst (decomp (Fun f T))  wfrestrictedvarsst (to_st 𝒜1)  V"
      using decomp_vars[of "Fun f T"] wfrestrictedvarsest_eq_wfrestrictedvarsst[of 𝒜1] by auto
    thus ?case
      using to_st_append[of 𝒜1 "[Decomp (Fun f T)]"]
            wf_append_suffix[OF Decompose.prems] Decompose.hyps(3)
      by (metis append_Nil2 decomp_vars(1,2) to_st.simps(1,3))
  qed
qed metis

private lemma pts_symbolic_c_preserves_tfrset:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')"
    and "tfrset (((trmsst ` 𝒮))  (trmsest 𝒜))"
    and "wftrms (((trmsst ` 𝒮))  (trmsest 𝒜))"
  shows "tfrset (((trmsst ` 𝒮'))  (trmsest 𝒜'))  wftrms (((trmsst ` 𝒮'))  (trmsest 𝒜'))"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  from step.hyps(2) step.IH[OF step.prems] show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Nil
    hence "(trmsst ` 𝒮1) = (trmsst ` 𝒮2)" by force
    thus ?case using Nil by metis
  next
    case (Decompose f T)
    obtain t where t: "t  ikest 𝒜1  assignment_rhsest 𝒜1" "Fun f T  t"
      using Decompose.hyps(1) by auto
    have t_wf: "wftrm t"
      using Decompose.prems wf_trm_subterm[of _ t]
            trmsest_ik_assignment_rhsI[OF t(1)]
      unfolding tfrset_def
      by (metis UN_E Un_iff)
    have "t  subtermsset (trmsest 𝒜1)" using trmsest_ik_assignment_rhsI t by auto
    hence "Fun f T  SMP (trmsest 𝒜1)"
      by (metis (no_types) SMP.MP SMP.Subterm UN_E t(2)) 
    hence "{Fun f T}  SMP (trmsest 𝒜1)" using SMP.Subterm[of "Fun f T"] by auto
    moreover have "trmsest 𝒜2 = insert (Fun f T) (trmsest 𝒜1)"
      using Decompose.hyps(3) by auto
    ultimately have *: "SMP (trmsest 𝒜1) = SMP (trmsest 𝒜2)"
      using SMP_subset_union_eq[of "{Fun f T}"]
      by (simp add: Un_commute)
    hence "SMP (((trmsst ` 𝒮1))  (trmsest 𝒜1)) = SMP (((trmsst ` 𝒮2))  (trmsest 𝒜2))"
      using Decompose.hyps(2) SMP_union by auto
    moreover have "t  trmsest 𝒜1. wftrm t" "wftrm (Fun f T)"
      using Decompose.prems wf_trm_subterm t(2) t_wf unfolding tfrset_def by auto
    hence "t  trmsest 𝒜2. wftrm t" by (metis * SMP.MP SMP_wf_trm) 
    hence "t  ((trmsst ` 𝒮2))  (trmsest 𝒜2). wftrm t"
      using Decompose.prems Decompose.hyps(2) unfolding tfrset_def by force
    ultimately show ?thesis using Decompose.prems unfolding tfrset_def by presburger 
  qed (metis trmsst_updatest_eq_snd, metis trmsst_updatest_eq_rcv,
       metis trmsst_updatest_eq_eq, metis trmsst_updatest_eq_ineq)
qed metis

private lemma pts_symbolic_c_preserves_tfrstp:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')" "S  𝒮  {to_st 𝒜}. list_all tfrstp S"
  shows "S  𝒮'  {to_st 𝒜'}. list_all tfrstp S"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  from step.hyps(2) step.IH[OF step.prems] show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Nil
    have 1: "S  {to_st 𝒜2}. list_all tfrstp S" using Nil by simp
    have 2: "𝒮2 = 𝒮1 - {[]}" "S  𝒮1. list_all tfrstp S"  using Nil by simp_all
    have "S  𝒮2. list_all tfrstp S"
    proof
      fix S assume "S  𝒮2"
      hence "S  𝒮1" using 2(1) by simp
      thus "list_all tfrstp S" using 2(2) by simp
    qed
    thus ?case using 1 by auto
  next
    case (Send t S)
    have 1: "S  {to_st 𝒜2}. list_all tfrstp S" using Send by (simp add: to_st_append)
    have 2: "𝒮2 = insert S (𝒮1 - {send⟨tst#S})" "S  𝒮1. list_all tfrstp S"  using Send by simp_all
    have 3: "S  𝒮2. list_all tfrstp S"
    proof
      fix S' assume "S'  𝒮2"
      hence "S'  𝒮1  S' = S" using 2(1) by auto
      moreover have "list_all tfrstp S" using Send.hyps 2(2) by auto
      ultimately show "list_all tfrstp S'" using 2(2) by blast
    qed
    thus ?case using 1 by auto
  next
    case (Receive t S)
    have 1: "S  {to_st 𝒜2}. list_all tfrstp S" using Receive by (simp add: to_st_append)
    have 2: "𝒮2 = insert S (𝒮1 - {receive⟨tst#S})" "S  𝒮1. list_all tfrstp S"
      using Receive by simp_all
    have 3: "S  𝒮2. list_all tfrstp S"
    proof
      fix S' assume "S'  𝒮2"
      hence "S'  𝒮1  S' = S" using 2(1) by auto
      moreover have "list_all tfrstp S" using Receive.hyps 2(2) by auto
      ultimately show "list_all tfrstp S'" using 2(2) by blast
    qed
    show ?case using 1 3 by auto
  next
    case (Equality a t t' S)
    have 1: "to_st 𝒜2 = to_st 𝒜1@[a: t  t'st]" "list_all tfrstp (to_st 𝒜1)"
      using Equality by (simp_all add: to_st_append)
    have 2: "list_all tfrstp [a: t  t'st]" using Equality by fastforce
    have 3: "list_all tfrstp (to_st 𝒜2)"
      using tfr_stp_all_append[of "to_st 𝒜1" "[a: t  t'st]"] 1 2 by metis
    hence 4: "S  {to_st 𝒜2}. list_all tfrstp S" using Equality by simp
    have 5: "𝒮2 = insert S (𝒮1 - {a: t  t'st#S})" "S  𝒮1. list_all tfrstp S"
      using Equality by simp_all
    have 6: "S  𝒮2. list_all tfrstp S" 
    proof
      fix S' assume "S'  𝒮2"
      hence "S'  𝒮1  S' = S" using 5(1) by auto
      moreover have "list_all tfrstp S" using Equality.hyps 5(2) by auto
      ultimately show "list_all tfrstp S'" using 5(2) by blast
    qed
    thus ?case using 4 by auto
  next
    case (Inequality X F S)
    have 1: "to_st 𝒜2 = to_st 𝒜1@[X⟨∨≠: Fst]" "list_all tfrstp (to_st 𝒜1)"
      using Inequality by (simp_all add: to_st_append)
    have "list_all tfrstp (X⟨∨≠: Fst#S)" using Inequality(1,4) by blast
    hence 2: "list_all tfrstp [X⟨∨≠: Fst]" by simp
    have 3: "list_all tfrstp (to_st 𝒜2)"
      using tfr_stp_all_append[of "to_st 𝒜1" "[X⟨∨≠: Fst]"] 1 2 by metis
    hence 4: "S  {to_st 𝒜2}. list_all tfrstp S" using Inequality by simp
    have 5: "𝒮2 = insert S (𝒮1 - {X⟨∨≠: Fst#S})" "S  𝒮1. list_all tfrstp S"
      using Inequality by simp_all
    have 6: "S  𝒮2. list_all tfrstp S"
    proof
      fix S' assume "S'  𝒮2"
      hence "S'  𝒮1  S' = S" using 5(1) by auto
      moreover have "list_all tfrstp S" using Inequality.hyps 5(2) by auto
      ultimately show "list_all tfrstp S'" using 5(2) by blast
    qed
    thus ?case using 4 by auto
  next
    case (Decompose f T)
    hence 1: "S  𝒮2. list_all tfrstp S" by blast
    have 2: "list_all tfrstp (to_st 𝒜1)" "list_all tfrstp (to_st [Decomp (Fun f T)])"
      using Decompose.prems decomp_tfrstp by auto
    hence "list_all tfrstp (to_st 𝒜1@to_st [Decomp (Fun f T)])" by auto
    hence "list_all tfrstp (to_st 𝒜2)"
      using Decompose.hyps(3) to_st_append[of 𝒜1 "[Decomp (Fun f T)]"]
      by auto
    thus ?case using 1 by blast
  qed
qed

private lemma pts_symbolic_c_preserves_well_analyzed:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')" "well_analyzed 𝒜"
  shows "well_analyzed 𝒜'"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  from step.hyps(2) step.IH[OF step.prems] show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Receive thus ?case by (metis well_analyzed_singleton(1) well_analyzed_append)
  next
    case Send thus ?case by (metis well_analyzed_singleton(2) well_analyzed_append)
  next
    case Equality thus ?case by (metis well_analyzed_singleton(3) well_analyzed_append)
  next
    case Inequality thus ?case by (metis well_analyzed_singleton(4) well_analyzed_append)
  next
    case (Decompose f T)
    hence "Fun f T  subtermsset (ikest 𝒜1  assignment_rhsest 𝒜1) - (Var`𝒱)" by auto
    thus ?case by (metis well_analyzed.Decomp Decompose.prems Decompose.hyps(3))
  qed simp
qed metis

private lemma pts_symbolic_c_preserves_Ana_invar_subst:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')"
    and "Ana_invar_subst (
          ((ikst ` dualst ` 𝒮)  (ikest 𝒜)) 
          ((assignment_rhsst ` 𝒮)  (assignment_rhsest 𝒜)))"
  shows "Ana_invar_subst (
          ((ikst ` dualst ` 𝒮')  (ikest 𝒜')) 
          ((assignment_rhsst ` 𝒮')  (assignment_rhsest 𝒜')))"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  from step.hyps(2) step.IH[OF step.prems] show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Nil
    hence "(ikst ` dualst ` 𝒮1) = (ikst ` dualst ` 𝒮2)"
          "(assignment_rhsst ` 𝒮1) = (assignment_rhsst ` 𝒮2)"
      by force+
    thus ?case using Nil by metis
  next 
    case Send show ?case
      using ikst_updatest_subset_snd[OF Send.hyps]
            Ana_invar_subst_subset[OF Send.prems]
      by (metis Un_mono)
  next
    case Receive show ?case
      using ikst_updatest_subset_rcv[OF Receive.hyps]
            Ana_invar_subst_subset[OF Receive.prems]
      by (metis Un_mono)
  next
    case Equality show ?case
      using ikst_updatest_subset_eq[OF Equality.hyps]
            Ana_invar_subst_subset[OF Equality.prems]
      by (metis Un_mono)
  next
    case Inequality show ?case
      using ikst_updatest_subset_ineq[OF Inequality.hyps]
            Ana_invar_subst_subset[OF Inequality.prems]
      by (metis Un_mono)
  next
    case (Decompose f T)
    let ?X = "(assignment_rhsst`𝒮2)  assignment_rhsest 𝒜2"
    let ?Y = "(assignment_rhsst`𝒮1)  assignment_rhsest 𝒜1"
    obtain K M where Ana: "Ana (Fun f T) = (K,M)" by atomize_elim auto
    hence *: "ikest 𝒜2 = ikest 𝒜1  set M" "assignment_rhsest 𝒜2 = assignment_rhsest 𝒜1"
      using ikest_append assignment_rhsest_append decomp_ik
            decomp_assignment_rhs_empty Decompose.hyps(3)
      by auto
    { fix g S assume "Fun g S  subtermsset ((ikst`dualst`𝒮2)  ikest 𝒜2  ?X)"
      hence "Fun g S  subtermsset ((ikst`dualst ` 𝒮1)  ikest 𝒜1  set M  ?X)"
        using * Decompose.hyps(2) by auto
      hence "Fun g S  subtermsset ((ikst`dualst ` 𝒮1))
             Fun g S  subtermsset (ikest 𝒜1)
             Fun g S  subtermsset (set M)
             Fun g S  subtermsset ((assignment_rhsst`𝒮1))
             Fun g S  subtermsset (assignment_rhsest 𝒜1)"
        using Decompose * Ana_fun_subterm[OF Ana] by auto
      moreover have "Fun f T  subtermsset (ikest 𝒜1  assignment_rhsest 𝒜1)"
        using trmsest_ik_subtermsI Decompose.hyps(1) by auto 
      hence "subterms (Fun f T)  subtermsset (ikest 𝒜1  assignment_rhsest 𝒜1)"
        by (metis in_subterms_subset_Union)
      hence "subtermsset (set M)  subtermsset (ikest 𝒜1  assignment_rhsest 𝒜1)"
        by (meson Un_upper2 Ana_subterm[OF Ana] subterms_subset_set psubsetE subset_trans)
      ultimately have "Fun g S  subtermsset ((ikst`dualst ` 𝒮1)  ikest 𝒜1  ?Y)"
        by auto
    }
    thus ?case using Decompose unfolding Ana_invar_subst_def by metis
  qed
qed

private lemma pts_symbolic_c_preserves_constr_disj_vars:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')" "wfsts' 𝒮 𝒜" "fvest 𝒜  bvarsest 𝒜 = {}"
  shows "fvest 𝒜'  bvarsest 𝒜' = {}"
using assms
proof (induction rule: rtranclp_induct2)
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  have *: "S. S  𝒮1  fvst S  bvarsest 𝒜1 = {}" "S. S  𝒮1  fvest 𝒜1  bvarsst S = {}"
    using pts_symbolic_c_preserves_wf_prot[OF step.hyps(1) step.prems(1)]
    unfolding wfsts'_def by auto
  from step.hyps(2) step.IH[OF step.prems]
  show ?case
  proof (induction rule: pts_symbolic_c_induct)
    case Nil thus ?case by auto
  next 
    case (Send ts S)
    hence "fvest 𝒜2 = fvest 𝒜1  fvset (set ts)" "bvarsest 𝒜2 = bvarsest 𝒜1"
          "fvst (send⟨tsst#S) = fvset (set ts)  fvst S"
      using fvest_append bvarsest_append by simp+
    thus ?case using *(1)[OF Send(1)] Send(4) by auto
  next
    case (Receive ts S)
    hence "fvest 𝒜2 = fvest 𝒜1  fvset (set ts)" "bvarsest 𝒜2 = bvarsest 𝒜1"
          "fvst (receive⟨tsst#S) = fvset (set ts)  fvst S"
      using fvest_append bvarsest_append by simp+
    thus ?case using *(1)[OF Receive(1)] Receive(4) by auto
  next
    case (Equality a t t' S)
    hence "fvest 𝒜2 = fvest 𝒜1  fv t  fv t'" "bvarsest 𝒜2 = bvarsest 𝒜1"
          "fvst (a: t  t'st#S) = fv t  fv t'  fvst S"
      using fvest_append bvarsest_append by fastforce+
    thus ?case using *(1)[OF Equality(1)] Equality(4) by auto
  next
    case (Inequality X F S)
    hence "fvest 𝒜2 = fvest 𝒜1  (fvpairs F - set X)" "bvarsest 𝒜2 = bvarsest 𝒜1  set X"
          "fvst (X⟨∨≠: Fst#S) = (fvpairs F - set X)  fvst S"
      using fvest_append bvarsest_append strand_vars_split(3)[of "[X⟨∨≠: Fst]" S]
      by auto+
    moreover have "fvest 𝒜1  set X = {}" using *(2)[OF Inequality(1)] by auto
    ultimately show ?case using *(1)[OF Inequality(1)] Inequality(4) by auto
  next
    case (Decompose f T)
    thus ?case
      using Decompose(3,4) bvars_decomp ik_assignment_rhs_decomp_fv[OF Decompose(1)] by auto
  qed
qed


subsubsection ‹Theorem: The Typing Result Lifted to the Transition System Level›
private lemma wfsts'_decomp_rm:
  assumes "well_analyzed A" "wfsts' S (decomp_rmest A)" shows "wfsts' S A"
unfolding wfsts'_def
proof (intro conjI)
  show "SS. wfst (wfrestrictedvarsest A) (dualst S)"
    by (metis (no_types) assms(2) wfsts'_def wfrestrictedvarsest_decomp_rmest_subset
                wf_vars_mono le_iff_sup)

  show "SaS. S'S. fvst Sa  bvarsst S' = {}" by (metis assms(2) wfsts'_def)

  show "SS. fvst S  bvarsest A = {}" by (metis assms(2) wfsts'_def bvars_decomp_rm)

  show "SS. fvest A  bvarsst S = {}" by (metis assms wfsts'_def well_analyzed_decomp_rmest_fv)
qed

private lemma decompsest_pts_symbolic_c:
  assumes "D  decompsest (ikest A) (assignment_rhsest A) "
  shows "(S,A) c* (S,A@D)"
using assms(1)
proof (induction D rule: decompsest.induct)
  case (Decomp B f X K T)
  have "subtermsset (ikest A  assignment_rhsest A) 
        subtermsset (ikest (A@B)  assignment_rhsest (A@B))"
    using ikest_append[of A B] assignment_rhsest_append[of A B]
    by auto
  hence "Fun f X  subtermsset (ikest (A@B)  assignment_rhsest (A@B))" using Decomp.hyps by auto
  hence "(S,A@B) c (S,A@B@[Decomp (Fun f X)])"
    using pts_symbolic_c.Decompose[of f X "A@B"]
    by simp
  thus ?case
    using Decomp.IH rtrancl_into_rtrancl
          rtranclp_rtrancl_eq[of pts_symbolic_c "(S,A)" "(S,A@B)"]
    by auto
qed simp

private lemma pts_symbolic_to_pts_symbolic_c:
  assumes "(𝒮,to_st (decomp_rmest 𝒜d)) * (𝒮',𝒜')" "semest_d {}  (to_est 𝒜')" "semest_c {}  𝒜d"
  and wf: "wfsts' 𝒮 (decomp_rmest 𝒜d)" "wfest {} 𝒜d"
  and tar: "Ana_invar_subst (((ikst` dualst` 𝒮)  (ikest 𝒜d))
                             ((assignment_rhsst` 𝒮)  (assignment_rhsest 𝒜d)))"
  and wa: "well_analyzed 𝒜d"
  and : "interpretationsubst "
  shows "𝒜d'. 𝒜' = to_st (decomp_rmest 𝒜d')  (𝒮,𝒜d) c* (𝒮',𝒜d')  semest_c {}  𝒜d'"
using assms(1,2)
proof (induction rule: rtranclp_induct2)
  case refl thus ?case using assms by auto
next
  case (step 𝒮1 𝒜1 𝒮2 𝒜2)
  have "semest_d {}  (to_est 𝒜1)" using step.hyps(2) step.prems
    by (induct rule: pts_symbolic_induct, metis, (metis semest_d_split_left to_est_append)+)
  then obtain 𝒜1d where
      𝒜1d: "𝒜1 = to_st (decomp_rmest 𝒜1d)" "(𝒮, 𝒜d) c* (𝒮1, 𝒜1d)" "semest_c {}  𝒜1d"
    using step.IH by atomize_elim auto

  show ?case using step.hyps(2)
  proof (induction rule: pts_symbolic_induct)
    case Nil
    hence "(𝒮, 𝒜d) c* (𝒮2, 𝒜1d)" using 𝒜1d pts_symbolic_c.Nil[OF Nil.hyps(1), of 𝒜1d] by simp
    thus ?case using 𝒜1d Nil by auto
  next
    case (Send t S)
    hence "semest_c {}  (𝒜1d@[Step (receive⟨tst)])" using semest_c.Receive[OF 𝒜1d(3)] by simp
    moreover have "(𝒮1, 𝒜1d) c (𝒮2, 𝒜1d@[Step (receive⟨tst)])"
      using Send.hyps(2) pts_symbolic_c.Send[OF Send.hyps(1), of 𝒜1d] by simp
    moreover have "to_st (decomp_rmest (𝒜1d@[Step (receive⟨tst)])) = 𝒜2"
      using Send.hyps(3) decomp_rmest_append 𝒜1d(1) by (simp add: to_st_append) 
    ultimately show ?case using 𝒜1d(2) by auto      
  next
    case (Equality a t t' S)
    hence "t   = t'  "
      using step.prems semest_d_eq_sem_st[of "{}"  "to_est 𝒜2"]
            to_st_append to_est_append to_st_to_est_inv
      by auto
    hence "semest_c {}  (𝒜1d@[Step (a: t  t'st)])" using semest_c.Equality[OF 𝒜1d(3)] by simp
    moreover have "(𝒮1, 𝒜1d) c (𝒮2, 𝒜1d@[Step (a: t  t'st)])"
      using Equality.hyps(2) pts_symbolic_c.Equality[OF Equality.hyps(1), of 𝒜1d] by simp
    moreover have "to_st (decomp_rmest (𝒜1d@[Step (a: t  t'st)])) = 𝒜2"
      using Equality.hyps(3) decomp_rmest_append 𝒜1d(1) by (simp add: to_st_append) 
    ultimately show ?case using 𝒜1d(2) by auto
  next
    case (Inequality X F S)
    hence "ineq_model  X F"
      using step.prems semest_d_eq_sem_st[of "{}"  "to_est 𝒜2"]
            to_st_append to_est_append to_st_to_est_inv
      by auto
    hence "semest_c {}  (𝒜1d@[Step (X⟨∨≠: Fst)])" using semest_c.Inequality[OF 𝒜1d(3)] by simp
    moreover have "(𝒮1, 𝒜1d) c (𝒮2, 𝒜1d@[Step (X⟨∨≠: Fst)])"
      using Inequality.hyps(2) pts_symbolic_c.Inequality[OF Inequality.hyps(1), of 𝒜1d] by simp
    moreover have "to_st (decomp_rmest (𝒜1d@[Step (X⟨∨≠: Fst)])) = 𝒜2"
      using Inequality.hyps(3) decomp_rmest_append 𝒜1d(1) by (simp add: to_st_append) 
    ultimately show ?case using 𝒜1d(2) by auto
  next
    case (Receive ts S)
    hence "t  set ts. ikst 𝒜1 set   t  "
      using step.prems semest_d_eq_sem_st[of "{}"  "to_est 𝒜2"]
            strand_sem_split(4)[of "{}" 𝒜1 "[send⟨tsst]" ]
            to_st_append to_est_append to_st_to_est_inv
      by auto
    moreover have "ikst 𝒜1 set   ikest 𝒜1d set " using 𝒜1d(1) decomp_rmest_ik_subset by auto
    ultimately have *: "t  set ts. ikest 𝒜1d set   t  "
      using ideduct_mono by auto

    have "wfsts' 𝒮 𝒜d" by (rule wfsts'_decomp_rm[OF wa assms(4)])
    hence **: "wfest {} 𝒜1d" by (rule pts_symbolic_c_preserves_wf_is[OF 𝒜1d(2) _ assms(5)])

    have "Ana_invar_subst ((ikst`dualst`𝒮1)  (ikest 𝒜1d) 
                           ((assignment_rhsst`𝒮1)  (assignment_rhsest 𝒜1d)))"
      using tar 𝒜1d(2) pts_symbolic_c_preserves_Ana_invar_subst by metis
    hence "Ana_invar_subst (ikest 𝒜1d)" "Ana_invar_subst (assignment_rhsest 𝒜1d)"
      using Ana_invar_subst_subset by blast+
    moreover have "well_analyzed 𝒜1d"
      using pts_symbolic_c_preserves_well_analyzed[OF 𝒜1d(2) wa] by metis
    ultimately obtain D where D:
        "D  decompsest (ikest 𝒜1d) (assignment_rhsest 𝒜1d) "
        "t  set ts. ikest (𝒜1d@D) set  c t  "
      using decompsest_exist_subst_list[OF * 𝒜1d(3) ** assms(8)]
      unfolding Ana_invar_subst_def by auto
    
    have "(𝒮, 𝒜d) c* (𝒮1, 𝒜1d@D)" using 𝒜1d(2) decompsest_pts_symbolic_c[OF D(1), of 𝒮1] by auto
    hence "(𝒮, 𝒜d) c* (𝒮2, 𝒜1d@D@[Step (send⟨tsst)])"
      using Receive(2) pts_symbolic_c.Receive[OF Receive.hyps(1), of "𝒜1d@D"] by auto
    moreover have "𝒜2 = to_st (decomp_rmest (𝒜1d@D@[Step (send⟨tsst)]))"
      using Receive.hyps(3) 𝒜1d(1) decompsest_decomp_rmest_empty[OF D(1)]
            decomp_rmest_append to_st_append
      by auto
    moreover have "semest_c {}  (𝒜1d@D@[Step (send⟨tsst)])"
      using D(2) semest_c.Send[OF semest_c_decompsest_append[OF 𝒜1d(3) D(1)]] by simp
    ultimately show ?case by auto
  qed
qed

private lemma pts_symbolic_c_to_pts_symbolic:
  assumes "(𝒮,𝒜) c* (𝒮',𝒜')" "semest_c {}  𝒜'"
  shows "(𝒮,to_st (decomp_rmest 𝒜)) * (𝒮',to_st (decomp_rmest 𝒜'))"
        "semest_d {}  (decomp_rmest 𝒜')"
proof -
  show "(𝒮,to_st (decomp_rmest 𝒜)) * (𝒮',to_st (decomp_rmest 𝒜'))" using assms(1)
  proof (induction rule: rtranclp_induct2)
    case (step 𝒮1 𝒜1 𝒮2 𝒜2) show ?case using step.hyps(2,1) step.IH
    proof (induction rule: pts_symbolic_c_induct)
      case Nil thus ?case
        using pts_symbolic.Nil[OF Nil.hyps(1), of "to_st (decomp_rmest 𝒜1)"] by simp
    next
      case (Send t S) thus ?case
        using pts_symbolic.Send[OF Send.hyps(1), of "to_st (decomp_rmest 𝒜1)"]
        by (simp add: decomp_rmest_append to_st_append)
    next
      case (Receive t S) thus ?case
        using pts_symbolic.Receive[OF Receive.hyps(1), of "to_st (decomp_rmest 𝒜1)"] 
        by (simp add: decomp_rmest_append to_st_append)
    next
      case (Equality a t t' S) thus ?case
        using pts_symbolic.Equality[OF Equality.hyps(1), of "to_st (decomp_rmest 𝒜1)"] 
        by (simp add: decomp_rmest_append to_st_append)
    next
      case (Inequality t t' S) thus ?case
        using pts_symbolic.Inequality[OF Inequality.hyps(1), of "to_st (decomp_rmest 𝒜1)"] 
        by (simp add: decomp_rmest_append to_st_append)
    next
      case (Decompose t) thus ?case using decomp_rmest_append by simp
    qed
  qed simp
qed (rule semest_d_decomp_rmest_if_semest_c[OF assms(2)])

private lemma pts_symbolic_to_pts_symbolic_c_from_initial:
  assumes "(𝒮0,[]) * (𝒮,𝒜)" "  𝒜" "wfsts' 𝒮0 []"
  and "Ana_invar_subst ((ikst ` dualst ` 𝒮0)  (assignment_rhsst ` 𝒮0))" "interpretationsubst "
  shows "𝒜d. 𝒜 = to_st (decomp_rmest 𝒜d)  (𝒮0,[]) c* (𝒮,𝒜d)  ( c to_st 𝒜d)"
using assms pts_symbolic_to_pts_symbolic_c[of 𝒮0 "[]" 𝒮 𝒜 ]
      semest_c_eq_sem_st[of "{}" ] semest_d_eq_sem_st[of "{}" ]
      to_st_to_est_inv[of 𝒜] strand_sem_eq_defs
by (auto simp add: constr_sem_c_def constr_sem_d_def simp del: subst_range.simps)

private lemma pts_symbolic_c_to_pts_symbolic_from_initial:
  assumes "(𝒮0,[]) c* (𝒮,𝒜)" " c to_st 𝒜"
  shows "(𝒮0,[]) * (𝒮,to_st (decomp_rmest 𝒜))" "  to_st (decomp_rmest 𝒜)"
using assms pts_symbolic_c_to_pts_symbolic[of 𝒮0 "[]" 𝒮 𝒜 ]
      semest_c_eq_sem_st[of "{}" ] semest_d_eq_sem_st[of "{}" ] strand_sem_eq_defs
by (auto simp add: constr_sem_c_def constr_sem_d_def)

private lemma to_st_trms_wf:
  assumes "wftrms (trmsest A)"
  shows "wftrms (trmsst (to_st A))"
using assms
proof (induction A)
  case (Cons x A)
  hence IH: "t  trmsst (to_st A). wftrm t" by auto
  with Cons show ?case
  proof (cases x)
    case (Decomp t)
    hence "wftrm t" using Cons.prems by auto
    obtain K T where Ana_t: "Ana t = (K,T)" by atomize_elim auto
    hence "trmsst (decomp t)  {t}  set K  set T" using decomp_set_unfold[OF Ana_t] by force
    moreover have "t  set T. wftrm t" using Ana_subterm[OF Ana_t] wftrm t wf_trm_subterm by auto
    ultimately have "t  trmsst (decomp t). wftrm t" using Ana_keys_wf'[OF Ana_t] wftrm t by auto
    thus ?thesis using IH Decomp by auto
  qed auto
qed simp

private lemma to_st_trms_SMP_subset: "trmsst (to_st A)  SMP (trmsest A)"
proof
  fix t assume "t  trmsst (to_st A)" thus "t  SMP (trmsest A)"
  proof (induction A)
    case (Cons x A)
    hence *: "t  trmsst (to_st [x])  trmsst (to_st A)" using to_st_append[of "[x]" A] by auto
    have **: "trmsst (to_st A)  trmsst (to_st (x#A))" "trmsest A  trmsest (x#A)"
      using to_st_append[of "[x]" A] by auto
    show ?case
    proof (cases "t  trmsst (to_st A)")
      case True thus ?thesis using Cons.IH SMP_mono[OF **(2)] by auto
    next
      case False
      hence ***: "t  trmsst (to_st [x])" using * by auto
      thus ?thesis
      proof (cases x)
        case (Decomp t')
        hence ****: "t  trmsst (decomp t')" "t'  trmsest (x#A)" using *** by auto
        obtain K T where Ana_t': "Ana t' = (K,T)" by atomize_elim auto
        hence "t  {t'}  set K  set T" using decomp_set_unfold[OF Ana_t'] ****(1) by force
        moreover
        { assume "t = t'" hence ?thesis using SMP.MP[OF ****(2)] by simp }
        moreover
        { assume "t  set K" hence ?thesis using SMP.Ana[OF SMP.MP[OF ****(2)] Ana_t'] by auto }
        moreover
        { assume "t  set T" "t  t'"
          hence "t  t'" using Ana_subterm[OF Ana_t'] by blast
          hence ?thesis using SMP.Subterm[OF SMP.MP[OF ****(2)]] by auto
        } 
        ultimately show ?thesis using Decomp by auto
      qed auto
    qed
  qed simp
qed

private lemma to_st_trms_tfrset:
  assumes "tfrset (trmsest A)"
  shows "tfrset (trmsst (to_st A))"
proof -
  have *: "trmsst (to_st A)  SMP (trmsest A)"
    using to_st_trms_wf to_st_trms_SMP_subset assms unfolding tfrset_def by auto
  have "trmsst (to_st A) = trmsst (to_st A)  trmsest A" by (blast dest!: trmsestD)
  hence "SMP (trmsest A) = SMP (trmsst (to_st A))" using SMP_subset_union_eq[OF *] by auto
  thus ?thesis using * assms unfolding tfrset_def by presburger
qed

theorem wt_attack_if_tfr_attack_pts:
  assumes "wfsts 𝒮0" "tfrset ((trmsst ` 𝒮0))" "wftrms ((trmsst ` 𝒮0))" "S  𝒮0. list_all tfrstp S"
  and "Ana_invar_subst ((ikst ` dualst ` 𝒮0)  (assignment_rhsst ` 𝒮0))"
  and "(𝒮0,[]) * (𝒮,𝒜)" "interpretationsubst " "  𝒜, Var"
  shows "τ. interpretationsubst τ  (τ  𝒜, Var)  wtsubst τ  wftrms (subst_range τ)"
proof -
  have "((trmsst ` 𝒮0))  (trmsest []) = (trmsst ` 𝒮0)" "to_st [] = []" "list_all tfrstp []"
    using assms by simp_all
  hence *: "tfrset (((trmsst ` 𝒮0))  (trmsest []))"
           "wftrms (((trmsst ` 𝒮0))  (trmsest []))"
           "wfsts' 𝒮0 []" "S  𝒮0  {to_st []}. list_all tfrstp S"
    using assms wfsts_wfsts' by (metis, metis, metis, simp)

  obtain 𝒜d where 𝒜d: "𝒜 = to_st (decomp_rmest 𝒜d)" "(𝒮0,[]) c* (𝒮,𝒜d)" " c to_st 𝒜d"
    using pts_symbolic_to_pts_symbolic_c_from_initial assms *(3) by metis
  hence "tfrset ((trmsst ` 𝒮)  (trmsest 𝒜d))" "wftrms ((trmsst ` 𝒮)  (trmsest 𝒜d))"
    using pts_symbolic_c_preserves_tfrset[OF _ *(1,2)] by blast+
  hence "tfrset (trmsest 𝒜d)" "wftrms (trmsest 𝒜d)"
    unfolding tfrset_def by (metis DiffE DiffI SMP_union UnCI, metis UnCI)
  hence "tfrset (trmsst (to_st 𝒜d))" "wftrms (trmsst (to_st 𝒜d))"
    by (metis to_st_trms_tfrset, metis to_st_trms_wf)
  moreover have "wfconstr (to_st 𝒜d) Var"
  proof -
    have "wtsubst Var" "wftrms (subst_range Var)" "subst_domain Var  varsest 𝒜d = {}"
         "range_vars Var  bvarsest 𝒜d = {}"
      by (simp_all add: range_vars_alt_def)
    moreover have "wfest {} 𝒜d"
      using pts_symbolic_c_preserves_wf_is[OF 𝒜d(2) *(3), of "{}"]
      by auto
    moreover have "fvst (to_st 𝒜d)  bvarsest 𝒜d = {}"
      using pts_symbolic_c_preserves_constr_disj_vars[OF 𝒜d(2)] assms(1) wfsts_wfsts'
      by fastforce
    ultimately show ?thesis unfolding wfconstr_def wfsubst_def by simp
  qed
  moreover have "list_all tfrstp (to_st 𝒜d)"
    using pts_symbolic_c_preserves_tfrstp[OF 𝒜d(2) *(4)] by blast
  moreover have "wtsubst Var" "wftrms (subst_range Var)" by simp_all
  ultimately obtain τ where τ:
      "interpretationsubst τ" "τ c to_st 𝒜d, Var" "wtsubst τ" "wftrms (subst_range τ)"
    using wt_attack_if_tfr_attack[OF assms(7) 𝒜d(3)]
          tfrset (trmsst (to_st 𝒜d)) list_all tfrstp (to_st 𝒜d)
    unfolding tfrst_def by metis
  hence "τ  𝒜, Var" using pts_symbolic_c_to_pts_symbolic_from_initial 𝒜d by metis
  thus ?thesis using τ(1,3,4) by metis
qed


subsubsection ‹Corollary: The Typing Result on the Level of Constraints›
text ‹There exists well-typed models of satisfiable type-flaw resistant constraints›
corollary wt_attack_if_tfr_attack_d:
  assumes "wfst {} 𝒜" "fvst 𝒜  bvarsst 𝒜 = {}" "tfrst 𝒜" "wftrms (trmsst 𝒜)"
  and "Ana_invar_subst (ikst 𝒜  assignment_rhsst 𝒜)"
  and "interpretationsubst " "  𝒜"
  shows "τ. interpretationsubst τ  (τ  𝒜)  wtsubst τ  wftrms (subst_range τ)"
proof -
  { fix S A have "({S},A) * ({},A@dualst S)"
    proof (induction S arbitrary: A)
      case Nil thus ?case using pts_symbolic.Nil[of "{[]}"] by auto
    next
      case (Cons x S)
      hence "({S}, A@dualst [x]) * ({}, A@dualst (x#S))"
        by (metis dualst_append List.append_assoc List.append_Nil List.append_Cons)
      moreover have "({x#S}, A)  ({S}, A@dualst [x])"
        using pts_symbolic.Send[of _ S "{x#S}"] pts_symbolic.Receive[of _ S "{x#S}"]
              pts_symbolic.Equality[of _ _ _ S "{x#S}"] pts_symbolic.Inequality[of _ _ S "{x#S}"]
        by (cases x) auto
      ultimately show ?case by simp
    qed
  }
  hence 0: "({dualst 𝒜},[]) * ({},𝒜)" using dualst_self_inverse by (metis List.append_Nil)

  have "fvst (dualst 𝒜)  bvarsst (dualst 𝒜) = {}" using assms(2) dualst_fv dualst_bvars by metis+
  hence 1: "wfsts {dualst 𝒜}" using assms(1,2) dualst_self_inverse[of 𝒜] unfolding wfsts_def by auto
  
  have "(trmsst ` {𝒜}) = trmsst 𝒜" "(trmsst ` {dualst 𝒜}) = trmsst (dualst 𝒜)" by auto
  hence "tfrset ((trmsst ` {𝒜}))" "wftrms ((trmsst ` {𝒜}))"
        "((trmsst ` {𝒜})) = (trmsst ` {dualst 𝒜})"
    using assms(3,4) unfolding tfrst_def
    by (metis, metis, metis dualst_trms_eq)
  hence 2: "tfrset ((trmsst ` {dualst 𝒜}))" and 3: "wftrms ((trmsst ` {dualst 𝒜}))" by metis+

  have 4: "S  {dualst 𝒜}. list_all tfrstp S"
    using dualst_tfrstp assms(3) unfolding tfrst_def by blast

  have "assignment_rhsst 𝒜 = assignment_rhsst (dualst 𝒜)"
    by (induct 𝒜 rule: assignment_rhsst.induct) auto
  hence 5: "Ana_invar_subst ((ikst`dualst`{dualst 𝒜})  (assignment_rhsst`{dualst 𝒜}))"
    using assms(5) dualst_self_inverse[of 𝒜] by auto

  show ?thesis by (rule wt_attack_if_tfr_attack_pts[OF 1 2 3 4 5 0 assms(6,7)])
qed

end

end

end