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 ∧ (∀x∈set 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" "∀x∈set Y. fv x = {}" 
          using Cons by atomize_elim auto
        hence "map Γ (y#Y) = x#X ∧ (∀x∈set (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 "∀s∈subst_range θ. ∀u∈subst_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 = [] ∨ (∃s∈set T. s ∉ Var ` set X)" by (metis Q2_def that)
        } moreover {
          assume "Fun f T = t" hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)"
            unfolding t_def using a'(2,3) by simp
        } moreover {
          assume "Fun f T = t'" hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)"
            unfolding t'_def using a'(2,3) by simp
        } moreover {
          assume "Fun f T = Fun a []" hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)" by simp
        } ultimately show "T = [] ∨ (∃s∈set 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; S⟧c (θ ∘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; S⟧c (θ ∘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; S⟧c (θ ∘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⟨K⟩st,receive⟨T⟩st])"

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⟨ts⟩st)) ⋅estp θ = Step (send⟨ts ⋅list θ⟩st)"
  "(Step (receive⟨ts⟩st)) ⋅estp θ = Step (receive⟨ts ⋅list θ⟩st)"
  "(Step (⟨a: t ≐ t'⟩st)) ⋅estp θ = Step (⟨a: (t ⋅ θ) ≐ (t' ⋅ θ)⟩st)"
  "(Step (∀X⟨∨≠: F⟩st)) ⋅estp θ = Step (∀X⟨∨≠: (F ⋅pairs rm_vars (set X) θ)⟩st)"
by simp_all

private lemma varsestp_subst_apply_simps[simp]:
  "varsestp ((Step (send⟨ts⟩st)) ⋅estp θ) = fvset (set ts ⋅set θ)"
  "varsestp ((Step (receive⟨ts⟩st)) ⋅estp θ) = fvset (set ts ⋅set θ)"
  "varsestp ((Step (⟨a: t ≐ t'⟩st)) ⋅estp θ) = fv (t ⋅ θ) ∪ fv (t' ⋅ θ)"
  "varsestp ((Step (∀X⟨∨≠: F⟩st)) ⋅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⟨ts⟩st)])"
| Receive: "semest_d M0 ℐ S ⟹ semest_d M0 ℐ (S@[Step (receive⟨t⟩st)])"
| 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⟨∨≠: F⟩st)])"
| 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⟨ts⟩st)])"
| Receive: "semest_c M0 ℐ S ⟹ semest_c M0 ℐ (S@[Step (receive⟨t⟩st)])"
| 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⟨∨≠: F⟩st)])"
| 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⟨ts⟩st)] ⋅est θ = [Step (Receive (ts ⋅list θ))]"
  "[Step (send⟨ts⟩st)] ⋅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⟨K⟩st,receive⟨M⟩st}"
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⟨ts⟩st)] = [Step (send⟨ts⟩st)]"
  "decomp_rmest [Step (receive⟨ts⟩st)] = [Step (receive⟨ts⟩st)]"
  "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 = (⋃m∈M. 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⟨ts⟩st)]" "well_analyzed [Step (receive⟨ts⟩st)]"
  "well_analyzed [Step (⟨a: t ≐ t'⟩st)]" "well_analyzed [Step (∀X⟨∨≠: F⟩st)]"
  "¬well_analyzed [Decomp t]"
proof -
  show "well_analyzed [Step (send⟨ts⟩st)]" "well_analyzed [Step (receive⟨ts⟩st)]"
       "well_analyzed [Step (⟨a: t ≐ t'⟩st)]" "well_analyzed [Step (∀X⟨∨≠: F⟩st)]"
    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⟨ts⟩st]"]
            to_st_append[of 𝒜 "[Step (send⟨ts⟩st)]"]
      by (simp add: sup.commute)
  next
    case (Receive M0 ℐ 𝒜 ts) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜" ℐ "[receive⟨ts⟩st]"]
            to_st_append[of 𝒜 "[Step (receive⟨ts⟩st)]"]
      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⟨∨≠: F⟩st]"]
            to_st_append[of 𝒜 "[Step (∀X⟨∨≠: F⟩st)]"]
      by (simp add: sup.commute)
  next
    case (Decompose M0 ℐ 𝒜 t K M)
    have "⟦M0 ∪ ikst (to_st 𝒜); decomp t⟧d' ℐ"
    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⟨K⟩st,receive⟨M⟩st]⟧d' ℐ"
        by auto
      thus ?thesis using Decompose.hyps(3) unfolding decomp_def by auto
    qed
    hence "⟦M0; to_st 𝒜@decomp t⟧d' ℐ"
      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⟨K⟩st,receive⟨M⟩st]"
        using Ana unfolding decomp_def by auto
      hence **: "ikest 𝒜 ∪ M0 ⋅set ℐ ⊢c t ⋅ ℐ" and "⟦ikest 𝒜 ∪ M0; [send⟨K⟩st]⟧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⟨ts⟩st]"]
            to_st_append[of 𝒜 "[Step (send⟨ts⟩st)]"]
      by (simp add: sup.commute)
  next
    case (Receive M0 ℐ 𝒜 ts) thus ?case
      using strand_sem_append'[of M0 "to_st 𝒜" ℐ "[receive⟨ts⟩st]"]
            to_st_append[of 𝒜 "[Step (receive⟨ts⟩st)]"]
      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⟨∨≠: F⟩st]"]
            to_st_append[of 𝒜 "[Step (∀X⟨∨≠: F⟩st)]"]
      by (auto simp add: sup.commute)
  next
    case (Decompose M0 ℐ 𝒜 t K M)
    have "⟦M0 ∪ ikst (to_st 𝒜); decomp t⟧c' ℐ"
    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⟨K⟩st,receive⟨M⟩st]⟧c' ℐ"
        by auto
      thus ?thesis using Decompose.hyps(3) unfolding decomp_def by auto
    qed
    hence "⟦M0; to_st 𝒜@decomp t⟧c' ℐ"
      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⟨ts⟩st#S ∈ 𝒮"
  shows "wfsts' (updatest 𝒮 (send⟨ts⟩st#S)) (𝒜@[Step (receive⟨ts⟩st)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "send⟨ts⟩st#S"
  let ?A = "𝒜@[Step (receive⟨ts⟩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: "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⟨ts⟩st#S ∈ 𝒮"
  shows "wfsts' (updatest 𝒮 (receive⟨ts⟩st#S)) (𝒜@[Step (send⟨ts⟩st)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "receive⟨ts⟩st#S"
  let ?A = "𝒜@[Step (send⟨ts⟩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: "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⟨∨≠: F⟩st#S ∈ 𝒮"
  shows "wfsts' (updatest 𝒮 (∀X⟨∨≠: F⟩st#S)) (𝒜@[Step (∀X⟨∨≠: F⟩st)])"
unfolding wfsts'_def
proof (intro conjI)
  let ?S = "∀X⟨∨≠: F⟩st#S"
  let ?A = "𝒜@[Step (∀X⟨∨≠: F⟩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: "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⟨∨≠: F⟩st # 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⟨ts⟩st#S ∈ 𝒮" "𝒮' = updatest 𝒮 (send⟨ts⟩st#S)" "𝒜' = 𝒜@[Step (receive⟨ts⟩st)]"
  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⟨ts⟩st#S ∈ 𝒮" "𝒮' = updatest 𝒮 (receive⟨ts⟩st#S)" "𝒜' = 𝒜@[Step (send⟨ts⟩st)]"
  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⟨∨≠: F⟩st#S ∈ 𝒮" "𝒮' = updatest 𝒮 (∀X⟨∨≠: F⟩st#S)" "𝒜' = 𝒜@[Step (∀X⟨∨≠: F⟩st)]"
  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⟨ts⟩st#S ∈ 𝒮"
          "𝒮' = updatest 𝒮 (send⟨ts⟩st#S)"
          "𝒜' = 𝒜@[Step (receive⟨ts⟩st)]"
  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⟨t⟩st#S ∈ 𝒮"
          "𝒮' = updatest 𝒮 (receive⟨t⟩st#S)"
          "𝒜' = 𝒜@[Step (send⟨t⟩st)]"
  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⟨∨≠: F⟩st#S ∈ 𝒮"
          "𝒮' = updatest 𝒮 (∀X⟨∨≠: F⟩st#S)"
          "𝒜' = 𝒜@[Step (∀X⟨∨≠: F⟩st)]"
  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⟨t⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙ (updatest 𝒮 (send⟨t⟩st#S),𝒜@[receive⟨t⟩st])"
| Receive[simp]:    "receive⟨t⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙ (updatest 𝒮 (receive⟨t⟩st#S),𝒜@[send⟨t⟩st])"
| Equality[simp]:   "⟨a: t ≐ t'⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙ (updatest 𝒮 (⟨a: t ≐ t'⟩st#S),𝒜@[⟨a: t ≐ t'⟩st])"
| Inequality[simp]: "∀X⟨∨≠: F⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙ (updatest 𝒮 (∀X⟨∨≠: F⟩st#S),𝒜@[∀X⟨∨≠: F⟩st])"

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⟨t⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙c (updatest 𝒮 (send⟨t⟩st#S),𝒜@[Step (receive⟨t⟩st)])"
| Receive[simp]:    "receive⟨t⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙c (updatest 𝒮 (receive⟨t⟩st#S),𝒜@[Step (send⟨t⟩st)])"
| Equality[simp]:   "⟨a: t ≐ t'⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙c (updatest 𝒮 (⟨a: t ≐ t'⟩st#S),𝒜@[Step (⟨a: t ≐ t'⟩st)])"
| Inequality[simp]: "∀X⟨∨≠: F⟩st#S ∈ 𝒮 ⟹ (𝒮,𝒜) ⇒∙c (updatest 𝒮 (∀X⟨∨≠: F⟩st#S),𝒜@[Step (∀X⟨∨≠: F⟩st)])"
| 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⟨t⟩st#S ∈ 𝒮; 𝒮' = updatest 𝒮 (send⟨t⟩st#S); 𝒜' = 𝒜@[receive⟨t⟩st]⟧ ⟹ P"
  and "⋀t S. ⟦receive⟨t⟩st#S ∈ 𝒮; 𝒮' = updatest 𝒮 (receive⟨t⟩st#S); 𝒜' = 𝒜@[send⟨t⟩st]⟧ ⟹ 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⟨∨≠: F⟩st#S ∈ 𝒮; 𝒮' = updatest 𝒮 (∀X⟨∨≠: F⟩st#S); 𝒜' = 𝒜@[∀X⟨∨≠: F⟩st]⟧ ⟹ 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⟨t⟩st#S ∈ 𝒮; 𝒮' = updatest 𝒮 (send⟨t⟩st#S); 𝒜' = 𝒜@[Step (receive⟨t⟩st)]⟧ ⟹ P"
  and "⋀t S. ⟦receive⟨t⟩st#S ∈ 𝒮; 𝒮' = updatest 𝒮 (receive⟨t⟩st#S); 𝒜' = 𝒜@[Step (send⟨t⟩st)]⟧ ⟹ 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⟨∨≠: F⟩st#S ∈ 𝒮; 𝒮' = updatest 𝒮 (∀X⟨∨≠: F⟩st#S); 𝒜' = 𝒜@[Step (∀X⟨∨≠: F⟩st)]⟧ ⟹ 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⟨ts⟩st#(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⟨t⟩st#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⟨t⟩st#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⟨∨≠: F⟩st]" "list_all tfrstp (to_st 𝒜1)"
      using Inequality by (simp_all add: to_st_append)
    have "list_all tfrstp (∀X⟨∨≠: F⟩st#S)" using Inequality(1,4) by blast
    hence 2: "list_all tfrstp [∀X⟨∨≠: F⟩st]" by simp
    have 3: "list_all tfrstp (to_st 𝒜2)"
      using tfr_stp_all_append[of "to_st 𝒜1" "[∀X⟨∨≠: F⟩st]"] 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⟨∨≠: F⟩st#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⟨ts⟩st#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⟨ts⟩st#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⟨∨≠: F⟩st#S) = (fvpairs F - set X) ∪ fvst S"
      using fvest_append bvarsest_append strand_vars_split(3)[of "[∀X⟨∨≠: F⟩st]" 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 "∀S∈S. wfst (wfrestrictedvarsest A) (dualst S)"
    by (metis (no_types) assms(2) wfsts'_def wfrestrictedvarsest_decomp_rmest_subset
                wf_vars_mono le_iff_sup)

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

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

  show "∀S∈S. 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⟨t⟩st)])" using semest_c.Receive[OF 𝒜1d(3)] by simp
    moreover have "(𝒮1, 𝒜1d) ⇒∙c (𝒮2, 𝒜1d@[Step (receive⟨t⟩st)])"
      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⟨t⟩st)])) = 𝒜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⟨∨≠: F⟩st)])" using semest_c.Inequality[OF 𝒜1d(3)] by simp
    moreover have "(𝒮1, 𝒜1d) ⇒∙c (𝒮2, 𝒜1d@[Step (∀X⟨∨≠: F⟩st)])"
      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⟨∨≠: F⟩st)])) = 𝒜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⟨ts⟩st]" ℐ]
            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⟨ts⟩st)])"
      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⟨ts⟩st)]))"
      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⟨ts⟩st)])"
      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