# Theory Typing_Result

```(*  Title:      Typing_Result.thy
Author:     Andreas Viktor Hess, DTU
*)

section ‹The 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 𝒞⇩p⇩u⇩b" "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_funs⇩s⇩t: "∃f. f ∉ funs⇩s⇩t (S::('fun,'var) strand)"
by (metis UNIV_eq_I finite_funs⇩s⇩t 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 ∧ wf⇩t⇩r⇩m (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 wf⇩t⇩r⇩m_def by auto
qed

lemma atype_ground_term_ex: "∃t. fv t = {} ∧ Γ t = TAtom a ∧ wf⇩t⇩r⇩m 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 moura
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" "wf⇩t⇩r⇩m τ"
shows "∃t. Γ t = τ ∧ wf⇩t⇩r⇩m t"
using assms
proof (induction τ)
case (Fun f Y)
have IH: "∃t. Γ t = y ∧ wf⇩t⇩r⇩m t" when y: "y ∈ set Y " for y
proof -
have "wf⇩t⇩r⇩m y"
using Fun y unfolding wf⇩t⇩r⇩m_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 wf⇩t⇩r⇩m_def by force+
moreover from IH have "∃X. map Γ X = Y ∧ (∀x ∈ set X. wf⇩t⇩r⇩m 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 wf⇩t⇩r⇩m_def in blast)

lemma type_pgwt_inhabited: "wf⇩t⇩r⇩m t ⟹ ∃t'. Γ t = Γ t' ∧ public_ground_wf_term t'"
proof -
assume "wf⇩t⇩r⇩m t"
{ fix τ assume "Γ t = τ"
hence "∃t'. Γ t = Γ t' ∧ public_ground_wf_term t'" using ‹wf⇩t⇩r⇩m 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› ‹wf⇩t⇩r⇩m 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 ‹wf⇩t⇩r⇩m 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 moura
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 ‹wf⇩t⇩r⇩m 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',θ')" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ"
and "list_all tfr⇩s⇩t⇩p S" "tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)"
shows "list_all tfr⇩s⇩t⇩p S'"
using assms
proof (induction rule: LI_rel.induct)
case (Compose S X f S' θ)
hence "list_all tfr⇩s⇩t⇩p S" "list_all tfr⇩s⇩t⇩p S'" by simp_all
moreover have "list_all tfr⇩s⇩t⇩p (map Send1 X)" by (induct X) auto
ultimately show ?case by simp
next
case (Unify S f Y δ X S' θ)
hence "list_all tfr⇩s⇩t⇩p (S@S')" by simp

have "fv⇩s⇩t (S@Send1 (Fun f X)#S') ∩ bvars⇩s⇩t (S@S') = {}"
using Unify.prems(1) by (auto simp add: wf⇩c⇩o⇩n⇩s⇩t⇩r_def)
moreover have "fv (Fun f X) ⊆ fv⇩s⇩t (S@Send1 (Fun f X)#S')" by auto
moreover have "fv (Fun f Y) ⊆ fv⇩s⇩t (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:
"bvars⇩s⇩t (S@S') ∩ fv (Fun f X) = {}" "bvars⇩s⇩t (S@S') ∩ fv (Fun f Y) = {}"
by blast+

have "wf⇩t⇩r⇩m (Fun f X)" using Unify.prems(5) by simp
moreover have "wf⇩t⇩r⇩m (Fun f Y)"
proof -
obtain x where "x ∈ set S" "Fun f Y ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t⇩p x)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p 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 (trms⇩s⇩t (S@Send1 (Fun f X)#S'))"
"Fun f Y ∈ SMP (trms⇩s⇩t (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 tfr⇩s⇩e⇩t_def by blast
ultimately have "wt⇩s⇩u⇩b⇩s⇩t δ" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis
moreover have "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using mgu_wf_trm[OF Unify.hyps(3)[symmetric] ‹wf⇩t⇩r⇩m (Fun f X)› ‹wf⇩t⇩r⇩m (Fun f Y)›]
by (metis wf_trm_subst_range_iff)
moreover have "bvars⇩s⇩t (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 tfr⇩s⇩t⇩p (S@S')›] by metis
next
case (Equality S δ t t' a S' θ)
have "list_all tfr⇩s⇩t⇩p (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 "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m t'" using Equality.prems(5) by auto
ultimately have "wt⇩s⇩u⇩b⇩s⇩t δ"
using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]]
by metis
moreover have "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using mgu_wf_trm[OF Equality.hyps(2)[symmetric] ‹wf⇩t⇩r⇩m t› ‹wf⇩t⇩r⇩m t'›]
by (metis wf_trm_subst_range_iff)
moreover have "fv⇩s⇩t (S@Equality a t t'#S') ∩ bvars⇩s⇩t (S@Equality a t t'#S') = {}"
using Equality.prems(1) by (auto simp add: wf⇩c⇩o⇩n⇩s⇩t⇩r_def)
hence "bvars⇩s⇩t (S@S') ∩ fv t = {}" "bvars⇩s⇩t (S@S') ∩ fv t' = {}" by auto
hence "bvars⇩s⇩t (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 tfr⇩s⇩t⇩p (S@S')›] by metis
qed

private lemma LI_in_SMP_subset_single:
assumes "(S,θ) ↝ (S',θ')" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ"
"tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)" "list_all tfr⇩s⇩t⇩p S"
and "trms⇩s⇩t S ⊆ SMP M"
shows "trms⇩s⇩t S' ⊆ SMP M"
using assms
proof (induction rule: LI_rel.induct)
case (Compose S X f S' θ)
hence "SMP (trms⇩s⇩t [Send1 (Fun f X)]) ⊆ SMP M"
proof -
have "SMP (trms⇩s⇩t [Send1 (Fun f X)]) ⊆ SMP (trms⇩s⇩t (S@Send1 (Fun f X)#S'))"
using trms⇩s⇩t_append SMP_mono by auto
thus ?thesis
using SMP_union[of "trms⇩s⇩t (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 (trms⇩s⇩t (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 ⟹ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p x)" "wf⇩t⇩r⇩m (Fun f X)"
using Unify.prems(4) by force+
moreover have "Fun f Y ∈ SMP (trms⇩s⇩t (S@Send1 (Fun f X)#S'))"
by (meson SMP_ikI Unify.hyps(2) contra_subsetD ik_append_subset(1))
ultimately have "wf⇩t⇩r⇩m (Fun f Y)" "Γ (Fun f X) = Γ (Fun f Y)"
using ik⇩s⇩t_subterm_exD[OF ‹Fun f Y ∈ ik⇩s⇩t S›] ‹tfr⇩s⇩e⇩t (trms⇩s⇩t (S@Send1 (Fun f X)#S'))›
unfolding tfr⇩s⇩e⇩t_def by (metis (full_types) SMP_wf_trm Unify.prems(4), blast)
hence "wt⇩s⇩u⇩b⇩s⇩t δ" by (metis mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric] ‹wf⇩t⇩r⇩m (Fun f X)›])
moreover have "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using mgu_wf_trm[OF Unify.hyps(3)[symmetric] ‹wf⇩t⇩r⇩m (Fun f X)› ‹wf⇩t⇩r⇩m (Fun f Y)›] by simp
ultimately have "trms⇩s⇩t ((S@Send1 (Fun f X)#S') ⋅⇩s⇩t δ) ⊆ 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 (trms⇩s⇩t (S@Equality a t t'#S'))" "t' ∈ SMP (trms⇩s⇩t (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 ⟹ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p x)" "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m t'"
using Equality.prems(4) by force+
ultimately have "wt⇩s⇩u⇩b⇩s⇩t δ" by (metis mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric] ‹wf⇩t⇩r⇩m t›])
moreover have "wf⇩t⇩r⇩m⇩s (subst_range δ)"
using mgu_wf_trm[OF Equality.hyps(2)[symmetric] ‹wf⇩t⇩r⇩m t› ‹wf⇩t⇩r⇩m t'›] by simp
ultimately have "trms⇩s⇩t ((S@Equality a t t'#S') ⋅⇩s⇩t δ) ⊆ 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',θ')" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
"tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)"
"list_all tfr⇩s⇩t⇩p S"
shows "tfr⇩s⇩e⇩t (trms⇩s⇩t S') ∧ wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S')"
using assms
proof (induction rule: LI_rel.induct)
case (Compose S X f S' θ)
let ?SMPmap = "SMP (trms⇩s⇩t (S@map Send1 X@S')) - (Var`𝒱)"
have "?SMPmap ⊆ SMP (trms⇩s⇩t (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 tfr⇩s⇩e⇩t_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 tfr⇩s⇩e⇩t_def by blast
next
case (Unify S f Y δ X S' θ)
let ?SMPδ = "SMP (trms⇩s⇩t (S@S' ⋅⇩s⇩t δ)) - (Var`𝒱)"

have "SMP (trms⇩s⇩t (S@S' ⋅⇩s⇩t δ)) ⊆ SMP (trms⇩s⇩t (S@Send1 (Fun f X)#S'))"
proof
fix s assume "s ∈ SMP (trms⇩s⇩t (S@S' ⋅⇩s⇩t δ))" thus "s ∈ SMP (trms⇩s⇩t (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 tfr⇩s⇩e⇩t_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 tfr⇩s⇩e⇩t_def by blast
next
case (Equality S δ t t' a S' θ)
let ?SMPδ = "SMP (trms⇩s⇩t (S@S' ⋅⇩s⇩t δ)) - (Var`𝒱)"

have "SMP (trms⇩s⇩t (S@S' ⋅⇩s⇩t δ)) ⊆ SMP (trms⇩s⇩t (S@Equality a t t'#S'))"
proof
fix s assume "s ∈ SMP (trms⇩s⇩t (S@S' ⋅⇩s⇩t δ))" thus "s ∈ SMP (trms⇩s⇩t (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 tfr⇩s⇩e⇩t_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 tfr⇩s⇩e⇩t_def by blast
qed

private lemma LI_preserves_welltypedness_single:
assumes "(S,θ) ↝ (S',θ')" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
and "tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)" "list_all tfr⇩s⇩t⇩p S"
shows "wt⇩s⇩u⇩b⇩s⇩t θ' ∧ wf⇩t⇩r⇩m⇩s (subst_range θ')"
using assms
proof (induction rule: LI_rel.induct)
case (Unify S f Y δ X S' θ)
have "wf⇩t⇩r⇩m (Fun f X)" using Unify.prems(5) unfolding tfr⇩s⇩e⇩t_def by simp
moreover have "wf⇩t⇩r⇩m (Fun f Y)"
proof -
obtain x where "x ∈ set S" "Fun f Y ∈ subterms⇩s⇩e⇩t (trms⇩s⇩t⇩p x)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t⇩p x)"
using Unify.hyps(2) Unify.prems(5) unfolding tfr⇩s⇩e⇩t_def by force
thus ?thesis using wf_trm_subterm by auto
qed
moreover have
"Fun f X ∈ SMP (trms⇩s⇩t (S@Send1 (Fun f X)#S'))" "Fun f Y ∈ SMP (trms⇩s⇩t (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 tfr⇩s⇩e⇩t_def by blast
ultimately have "wt⇩s⇩u⇩b⇩s⇩t δ" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis

have "wf⇩t⇩r⇩m⇩s (subst_range δ)"
by (meson mgu_wf_trm[OF Unify.hyps(3)[symmetric] ‹wf⇩t⇩r⇩m (Fun f X)› ‹wf⇩t⇩r⇩m (Fun f Y)›]
wf_trm_subst_range_iff)
hence "wf⇩t⇩r⇩m⇩s (subst_range (θ ∘⇩s δ))"
using wf_trm_subst_range_iff wf_trm_subst ‹wf⇩t⇩r⇩m⇩s (subst_range θ)›
unfolding subst_compose_def
by (metis (no_types, lifting))
thus ?case by (metis wt_subst_compose[OF ‹wt⇩s⇩u⇩b⇩s⇩t θ› ‹wt⇩s⇩u⇩b⇩s⇩t δ›])
next
case (Equality S δ t t' a S' θ)
have "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m t'" using Equality.prems(5) by simp_all
moreover have "Γ t = Γ t'"
using ‹list_all tfr⇩s⇩t⇩p (S@Equality a t t'#S')›
MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
by auto
ultimately have "wt⇩s⇩u⇩b⇩s⇩t δ" using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]] by metis

have "wf⇩t⇩r⇩m⇩s (subst_range δ)"
by (meson mgu_wf_trm[OF Equality.hyps(2)[symmetric] ‹wf⇩t⇩r⇩m t› ‹wf⇩t⇩r⇩m t'›] wf_trm_subst_range_iff)
hence "wf⇩t⇩r⇩m⇩s (subst_range (θ ∘⇩s δ))"
using wf_trm_subst_range_iff wf_trm_subst ‹wf⇩t⇩r⇩m⇩s (subst_range θ)›
unfolding subst_compose_def
by (metis (no_types, lifting))
thus ?case by (metis wt_subst_compose[OF ‹wt⇩s⇩u⇩b⇩s⇩t θ› ‹wt⇩s⇩u⇩b⇩s⇩t δ›])
qed metis

lemma LI_preserves_welltypedness:
assumes "(S,θ) ↝⇧* (S',θ')" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
and "tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)" "list_all tfr⇩s⇩t⇩p S"
shows "wt⇩s⇩u⇩b⇩s⇩t θ'" (is "?A θ'")
and "wf⇩t⇩r⇩m⇩s (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 "wf⇩c⇩o⇩n⇩s⇩t⇩r S2 θ2"
by (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)])
moreover have "tfr⇩s⇩e⇩t (trms⇩s⇩t S2)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S2)"
using LI_preserves_tfr_single[OF step.hyps(1)] step.prems by presburger+
moreover have "list_all tfr⇩s⇩t⇩p 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',θ')" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)"
and "tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)" "list_all tfr⇩s⇩t⇩p S"
shows "tfr⇩s⇩e⇩t (trms⇩s⇩t S')" (is "?A S'")
and "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S')" (is "?B S'")
and "list_all tfr⇩s⇩t⇩p 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 "wf⇩c⇩o⇩n⇩s⇩t⇩r S2 θ2" "tfr⇩s⇩e⇩t (trms⇩s⇩t S2)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S2)" "list_all tfr⇩s⇩t⇩p 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 "wt⇩s⇩u⇩b⇩s⇩t θ2" "wf⇩t⇩r⇩m⇩s (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 "tfr⇩s⇩t S"
shows "tfr⇩s⇩t (LI_preproc S)"
unfolding tfr⇩s⇩t_def
proof
have S: "tfr⇩s⇩e⇩t (trms⇩s⇩t S)" "list_all tfr⇩s⇩t⇩p S" using assms unfolding tfr⇩s⇩t_def by metis+

show "tfr⇩s⇩e⇩t (trms⇩s⇩t (LI_preproc S))" by (metis S(1) LI_preproc_trms_eq)

show "list_all tfr⇩s⇩t⇩p (LI_preproc S)" using S(2)
proof (induction S)
case (Cons x S)
have IH: "list_all tfr⇩s⇩t⇩p (LI_preproc S)" using Cons by simp
have x: "tfr⇩s⇩t⇩p 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 "interpretation⇩s⇩u⇩b⇩s⇩t ℐ" "wt⇩s⇩u⇩b⇩s⇩t ℐ" "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 wf⇩t⇩r⇩m_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 "interpretation⇩s⇩u⇩b⇩s⇩t ℐ" by metis
show "wt⇩s⇩u⇩b⇩s⇩t ℐ" unfolding wt⇩s⇩u⇩b⇩s⇩t_def using props by simp
show "subst_range ℐ ⊆ public_ground_wf_terms" by (auto simp add: props)
qed

lemma wt_grounding_subst_exists:
"∃θ. wt⇩s⇩u⇩b⇩s⇩t θ ∧ wf⇩t⇩r⇩m⇩s (subst_range θ) ∧ fv (t ⋅ θ) = {}"
proof -
obtain θ where θ: "interpretation⇩s⇩u⇩b⇩s⇩t θ" "wt⇩s⇩u⇩b⇩s⇩t θ" "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" "wf⇩t⇩r⇩m t"
shows "Γ (fresh_pgwt S (Γ t)) = Γ t"
proof -
let ?P = "λτ::('fun,'atom) term_type. wf⇩t⇩r⇩m τ ∧ (∀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" "wf⇩t⇩r⇩m t"
shows "{} ⊢⇩c fresh_pgwt S (Γ t)"
proof -
let ?P = "λτ::('fun,'atom) term_type. wf⇩t⇩r⇩m τ ∧ (∀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 wf⇩t⇩r⇩m_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" "wf⇩t⇩r⇩m t"
obtains c where "Fun c [] ⊑ fresh_pgwt S (Γ t)" "c ∉ S"
proof -
let ?P = "λτ::('fun,'atom) term_type. wf⇩t⇩r⇩m τ ∧ (∀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 wf⇩t⇩r⇩m_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" "wf⇩t⇩r⇩m t" "wf⇩t⇩r⇩m s" "funs_term s ⊆ S"
shows "s ∉ subterms (fresh_pgwt S (Γ t))"
proof -
let ?P = "λτ::('fun,'atom) term_type. wf⇩t⇩r⇩m τ ∧ (∀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 wf⇩t⇩r⇩m_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" "wf⇩t⇩r⇩m s" "wf⇩t⇩r⇩m⇩s 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)" "wf⇩t⇩r⇩m⇩s T"
shows "∃σ::('fun,'var) subst.
subst_domain σ = S
∧ bij_betw σ (subst_domain σ) (subst_range σ)
∧ subterms⇩s⇩e⇩t (subst_range σ) ⊆ {t. {} ⊢⇩c t} - T
∧ (∀s ∈ subst_range σ. ∀u ∈ subst_range σ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u)
∧ wt⇩s⇩u⇩b⇩s⇩t σ
∧ wf⇩t⇩r⇩m⇩s (subst_range σ)"
using assms
proof (induction rule: finite_induct)
case empty
have "subst_domain Var = {}"
"bij_betw Var (subst_domain Var) (subst_range Var)"
"subterms⇩s⇩e⇩t (subst_range Var) ⊆ {t. {} ⊢⇩c t} - T"
"∀s ∈ subst_range Var. ∀u ∈ subst_range Var. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
"wt⇩s⇩u⇩b⇩s⇩t Var"
"wf⇩t⇩r⇩m⇩s (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 σ)"
"subterms⇩s⇩e⇩t (subst_range σ) ⊆ {t. {} ⊢⇩c t} - T"
"∀s ∈ subst_range σ. ∀u ∈ subst_range σ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
"wt⇩s⇩u⇩b⇩s⇩t σ" "wf⇩t⇩r⇩m⇩s (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 **: "wf⇩t⇩r⇩m (Var x)" by simp
have ***: "wf⇩t⇩r⇩m⇩s (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 σ ⊆ subterms⇩s⇩e⇩t (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 "subterms⇩s⇩e⇩t (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 "wt⇩s⇩u⇩b⇩s⇩t θ" using θ t(1) σ(5) unfolding wt⇩s⇩u⇩b⇩s⇩t_def by auto
moreover have "wf⇩t⇩r⇩m⇩s (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
∧ wt⇩s⇩u⇩b⇩s⇩t σ
∧ wf⇩t⇩r⇩m⇩s (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" "wf⇩t⇩r⇩m (σ x)" using assms(3) const_type wf_trmI[of "[]"] by auto
hence "Γ (Var x) = Γ (σ x)" "wf⇩t⇩r⇩m (σ x)" using assms(3) σ(1) by force+
}
ultimately have "wt⇩s⇩u⇩b⇩s⇩t σ" "wf⇩t⇩r⇩m⇩s (subst_range σ)"
using wf_trm_subst_range_iff[of σ]
unfolding wt⇩s⇩u⇩b⇩s⇩t_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 []) `  𝒞⇩p⇩u⇩b) - T
∧ wt⇩s⇩u⇩b⇩s⇩t σ
∧ wf⇩t⇩r⇩m⇩s (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 []) `  𝒞⇩p⇩u⇩b) - T"
"wt⇩s⇩u⇩b⇩s⇩t Var"
"wf⇩t⇩r⇩m⇩s (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 []) `  𝒞⇩p⇩u⇩b) - T" "wt⇩s⇩u⇩b⇩s⇩t σ"
"wf⇩t⇩r⇩m⇩s (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 []) `  𝒞⇩p⇩u⇩b) - ?T'" "wt⇩s⇩u⇩b⇩s⇩t δ" "wf⇩t⇩r⇩m⇩s (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 []) ` 𝒞⇩p⇩u⇩b - T"
using σ(3) δ(3) θ by (auto simp add: subst_domain_def)
moreover have "wt⇩s⇩u⇩b⇩s⇩t θ" using σ(4) δ(4) θ unfolding wt⇩s⇩u⇩b⇩s⇩t_def by auto
moreover have "wf⇩t⇩r⇩m⇩s (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" "wf⇩c⇩o⇩n⇩s⇩t⇩r S θ" "wt⇩s⇩u⇩b⇩s⇩t θ" "wf⇩t⇩r⇩m⇩s (subst_range θ)" "wf⇩t⇩r⇩m⇩s (trms⇩s⇩t S)"
and ℐ': "∀X F. Inequality X F ∈ set S ⟶ ineq_model ℐ' X F"
"ground (subst_range ℐ')"
"subst_domain ℐ' = {x ∈ vars⇩s⇩t S. ∃X F. Inequality X F ∈ set S ∧ x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X}"
and tfr_stp_all: "list_all tfr⇩s⇩t⇩p S"
shows "∃ℐ. interpretation⇩s⇩u⇩b⇩s⇩t ℐ ∧ (ℐ ⊨⇩c ⟨S, θ⟩) ∧ wt⇩s⇩u⇩b⇩s⇩t ℐ ∧ wf⇩t⇩r⇩m⇩s (subst_range ℐ)"
proof -
from ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S θ› have "wf⇩s⇩t {} S" "subst_idem θ" and S_θ_disj: "∀v ∈ vars⇩s⇩t S. θ v = Var v"
using subst_idemI[of θ] unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_def wf⇩s⇩u⇩b⇩s⇩t_def by force+

obtain ℐ::"('fun,'var) subst"
where ℐ: "interpretation⇩s⇩u⇩b⇩s⇩t ℐ" "wt⇩s⇩u⇩b⇩s⇩t ℐ" "subst_range ℐ ⊆ public_ground_wf_terms"
using wt_interpretation_exists by blast
hence ℐ_deduct: "⋀x M. M ⊢⇩c ℐ x" and ℐ_wf_trm: "wf⇩t⇩r⇩m⇩s (subst_range ℐ)"
using pgwt_deducible pgwt_wellformed by fastforce+

let ?P = "λδ X. subst_domain δ = set X ∧ ground (subst_range δ)"
let ?Sineqsvars = "{x ∈ vars⇩s⇩t S. ∃X F. Inequality X F ∈ set S ∧ x ∈ fv⇩p⇩a⇩i⇩r⇩s F ∧ x ∉ set X}"
let ?Strms = "subterms⇩s⇩e⇩t (trms⇩s⇩t S)"

have finite_vars: "finite ?Sineqsvars" "finite ?Strms" "wf⇩t⇩r⇩m⇩s ?Strms"
using wf_trm_subtermeq assms(5) by fastforce+

define Q1 where "Q1 = (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
∀x ∈ fv⇩p⇩a⇩i⇩r⇩s 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 ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s 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 tfr⇩s⇩t⇩p_list_all_alt_def[of S] by blast

have S_fv_bvars_disj: "fv⇩s⇩t S ∩ bvars⇩s⇩t S = {}" using ‹wf⇩c⇩o⇩n⇩s⇩t⇩r S θ› unfolding wf⇩c⇩o⇩n⇩s⇩t⇩r_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 ‹wf⇩c⇩o⇩n⇩s⇩t⇩r 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: "subterms⇩s⇩e⇩t (subst_range σ) ⊆ {t. {} ⊢⇩c t} - ?Strms"
and σ_wt: "wt⇩s⇩u⇩b⇩s⇩t σ"
and σ_wf_trm: "wf⇩t⇩r⇩m⇩s (subst_range σ)"
using wt_bij_finite_subst_exists[OF finite_vars]
subst_inj_on_is_bij_betw subterm_inj_on_alt_def'
by moura

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 σ ⊆ subterms⇩s⇩e⇩t (subst_range σ)" by auto
hence "subst_range σ ⊆ public_ground_wf_terms - ?Strms"
and σ_pgwt_img:
"subst_range σ ⊆ public_ground_wf_terms"
"subterms⇩s⇩e⇩t (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 ⟹ fv⇩p⇩a⇩i⇩r⇩s 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 ⟶ fv⇩p⇩a⇩i⇩r⇩s 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 ` subterms⇩s⇩e⇩t (subst_range σ))"
using exists_fun_notin_funs_terms[OF subterms_union_finite[OF σ_finite_img]]
by moura
hence a': "⋀T. Fun a T ∉ subterms⇩s⇩e⇩t (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' ⊆ fv⇩p⇩a⇩i⇩r⇩s F"
unfolding t_def t'_def by force

have t_subterms: "subterms t ∪ subterms t' ⊆ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s 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 ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X. ∃c. σ x = Fun c []"
proof
fix x assume "Q1 F X" and x: "x ∈ fv⇩p⇩a⇩i⇩r⇩s F - set X"
then obtain a where "Γ (Var x) = TAtom a" unfolding Q1_def by moura
hence a: "Γ (σ x) = TAtom a" using σ_wt unfolding wt⇩s⇩u⇩b⇩s⇩t_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: "subterms⇩s⇩e⇩t (subst_range σ) ∩ (subterms t ∪ subterms t') = {}"
proof -
define M1 where "M1 ≡ {t, t', Fun a []}"
define M2 where "M2 ≡ ?Strms"

have "subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F) ⊆ M2"
using F_in unfolding M2_def by force
moreover have "subterms t ∪ subterms t' ⊆ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s F) ∪ M1"
using t_subterms unfolding M1_def by blast
ultimately have *: "subterms t ∪ subterms t' ⊆ M2 ∪ M1"
by auto

have "subterms⇩s⇩e⇩t (subst_range σ) ∩ M1 = {}"
"subterms⇩s⇩e⇩t (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 ∈ subterms⇩s⇩e⇩t (trms⇩p⇩a⇩i⇩r⇩s 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': "fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s δ) ⊆ 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 "fv⇩p⇩a⇩i⇩r⇩s (g#G ⋅⇩p⇩a⇩i⇩r⇩s δ)  = fv (t ⋅ δ) ∪ fv (t' ⋅ δ) ∪ fv⇩p⇩a⇩i⇩r⇩s (G ⋅⇩p⇩a⇩i⇩r⇩s δ)"
"fv⇩p⇩a⇩i⇩r⇩s (g#G) = fv t ∪ fv t' ∪ fv⇩p⇩a⇩i⇩r⇩s 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 "fv⇩p⇩a⇩i⇩r⇩s (G ⋅⇩p⇩a⇩i⇩r⇩s δ) ⊆ 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: "fv⇩p⇩a⇩i⇩r⇩s ((F ⋅⇩p⇩a⇩i⇩r⇩s δ) ⋅⇩p⇩a⇩i⇩r⇩s σ) = {}"
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 ‹wf⇩s⇩t {} S› ‹simple S› S_θ_disj σ_ineqs_neq σ_ineqs_fv_dom' θ_vars_S_bvars_disj
proof (induction S arbitrary: M rule: wf⇩s⇩t_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 subst_apply_term.simps(1)
subst_subst_compose trm_subst_ident')

define M' where "M' ≡ M ∪ (ik⇩s⇩t S ⋅⇩s⇩e⇩t θ ∘⇩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 θ ∩ fv⇩p⇩a⇩i⇩r⇩s F = {}"
using ConsIneq.prems(1) subst_dom_vars_in_subst
by force
hence *: "F ⋅⇩p⇩a⇩i⇩r⇩s θ = F" by blast

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

have "⋀x. x ∈ vars⇩s⇩t S ⟹ x ∈ vars⇩s⇩t (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 "fv⇩p⇩a⇩i⇩r⇩s (F ⋅⇩p⇩a⇩i⇩r⇩s δ) ⊆ subst_domain σ" when "?P δ X" for δ
using ConsIneq.prems(3)[OF _ that] by simp
hence "fv⇩p⇩a⇩i⇩r⇩s F - set X ⊆ subst_domain σ"
using fv⇩p⇩a⇩i⇩r⇩s_subst_subset ex_P
by (metis Diff_subset_conv Un_commute)
thus ?thesis by (metis ineq_model_ground_subst[OF _ σ_i```