(*
(C) Copyright Andreas Viktor Hess, DTU, 2015-2018

All Rights Reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are
met:

- Redistributions of source code must retain the above copyright
  notice, this list of conditions and the following disclaimer.

- Redistributions in binary form must reproduce the above copyright
  notice, this list of conditions and the following disclaimer in the
  documentation and/or other materials provided with the distribution.

- Neither the name of the copyright holder nor the names of its
  contributors may be used to endorse or promote products
  derived from this software without specific prior written
  permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)

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

section {* Theory: The Lazy Intruder *}
theory LazyIntruder
imports StrandsAndConstraints IntruderDeduction InfiniteChains
begin

context intruder_model
begin

subsection {* Definition of the lazy intruder *}
inductive_set LI_rel::
    "((('fun,'var) strand \<times> (('fun,'var) subst)) \<times>
       ('fun,'var) strand \<times> (('fun,'var) subst)) set"
  and LI_rel' (infix "\<leadsto>" 50) 
  and LI_rel_trancl (infix "\<leadsto>\<^sup>+" 50)
  and LI_rel_rtrancl (infix "\<leadsto>\<^sup>*" 50)
where
  "A \<leadsto> B \<equiv> (A,B) \<in> LI_rel"
| "A \<leadsto>\<^sup>+ B \<equiv> (A,B) \<in> LI_rel\<^sup>+"
| "A \<leadsto>\<^sup>* B \<equiv> (A,B) \<in> LI_rel\<^sup>*"

| Compose: "\<lbrakk>simple S; length X = arity f; public f\<rbrakk>
            \<Longrightarrow> (S@snd\<langle>Fun f X\<rangle>#S',\<theta>) \<leadsto> (S@(map Send X)@S',\<theta>)"
| Unify: "\<lbrakk>simple S; Fun f Y \<in> ik\<^sub>s\<^sub>t S; Some \<delta> = mgu (Fun f X) (Fun f Y)\<rbrakk>
          \<Longrightarrow> (S@snd\<langle>Fun f X\<rangle>#S',\<theta>) \<leadsto> ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>,\<theta> \<circ>\<^sub>s \<delta>)"
| Equality: "\<lbrakk>simple S; Some \<delta> = mgu t t'\<rbrakk>
          \<Longrightarrow> (S@t \<doteq> t'#S',\<theta>) \<leadsto> ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>,\<theta> \<circ>\<^sub>s \<delta>)"

lemma LI_rel_simps:
  assumes "simple S\<^sub>p\<^sub>r\<^sub>e"
  shows "(S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Fun f X\<rangle>#S\<^sub>s\<^sub>u\<^sub>f, \<theta>) \<leadsto> (S', \<theta>') \<longleftrightarrow>
          (S' = S\<^sub>p\<^sub>r\<^sub>e@map Send X@S\<^sub>s\<^sub>u\<^sub>f \<and> \<theta>' = \<theta> \<and> length X = arity f \<and> public f) \<or>
           (\<exists>\<delta> Y. S' = (S\<^sub>p\<^sub>r\<^sub>e@S\<^sub>s\<^sub>u\<^sub>f \<cdot>\<^sub>s\<^sub>t \<delta>) \<and> \<theta>' = \<theta> \<circ>\<^sub>s \<delta> \<and> Fun f Y \<in> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e
                \<and> Some \<delta> = mgu (Fun f X) (Fun f Y))"
  (is "?A = (?B \<or> ?C)")
proof
  assume ?A thus "?B \<or> ?C"
  proof cases
    case (Compose S'\<^sub>p\<^sub>r\<^sub>e X' f' S'\<^sub>s\<^sub>u\<^sub>f)
    hence "S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e" "X' = X" "f' = f" "S'\<^sub>s\<^sub>u\<^sub>f = S\<^sub>s\<^sub>u\<^sub>f"
      using simple_fun_prefix_unique[OF Compose(1,4)] \<open>simple S\<^sub>p\<^sub>r\<^sub>e\<close> by metis+
    thus "?B \<or> ?C" using Compose by metis
  next
    case (Unify S'\<^sub>p\<^sub>r\<^sub>e f' Y \<delta> X' S'\<^sub>s\<^sub>u\<^sub>f)
    hence "S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e" "X' = X" "f' = f" "S'\<^sub>s\<^sub>u\<^sub>f = S\<^sub>s\<^sub>u\<^sub>f"
      using simple_fun_prefix_unique[OF Unify(1,4)] \<open>simple S\<^sub>p\<^sub>r\<^sub>e\<close> by metis+
    thus "?B \<or> ?C" using Unify by metis
  next
    case (Equality S'\<^sub>p\<^sub>r\<^sub>e \<delta> t t' S'\<^sub>s\<^sub>u\<^sub>f)
    then obtain S where S: "S\<^sub>p\<^sub>r\<^sub>e = S'\<^sub>p\<^sub>r\<^sub>e@S \<or> S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e@S" using append_eq_append_conv2 by blast
    have "S\<^sub>p\<^sub>r\<^sub>e \<noteq> S'\<^sub>p\<^sub>r\<^sub>e" using Equality by auto
    hence "S \<noteq> []" using S by auto
    then obtain x S' where "S = x#S'" by (metis hd_Cons_tl)
    hence "x = t \<doteq> t' \<or> x = snd\<langle>Fun f X\<rangle>" "S\<^sub>p\<^sub>r\<^sub>e = S'\<^sub>p\<^sub>r\<^sub>e@x#S' \<or> S'\<^sub>p\<^sub>r\<^sub>e = S\<^sub>p\<^sub>r\<^sub>e@x#S'"
      using S Equality(1) by auto
    hence False using \<open>simple S\<^sub>p\<^sub>r\<^sub>e\<close> \<open>simple S'\<^sub>p\<^sub>r\<^sub>e\<close> S by auto
    thus "?B \<or> ?C" by rule
  qed
next
  assume "?B \<or> ?C" thus ?A using \<open>simple S\<^sub>p\<^sub>r\<^sub>e\<close> by (blast intro: Compose Unify)
qed

lemma LI_rel_lhs_unfold:
  assumes "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto> (S\<^sub>2,\<theta>\<^sub>2)"
  shows "(\<exists>S f X S'. simple S \<and> S\<^sub>1 = S@snd\<langle>Fun f X\<rangle>#S') \<or>
         (\<exists>S t t' S'. simple S \<and> S\<^sub>1 = S@t \<doteq> t'#S')"
using assms by (induct rule: LI_rel.induct) auto


subsection {* Theorem: The lazy intruder terminates *}
lemma LI_compose_measure_lt: "((S@(map Send X)@S',\<theta>\<^sub>1), (S@snd\<langle>Fun f X\<rangle>#S',\<theta>\<^sub>2)) \<in> measure\<^sub>s\<^sub>t"
using strand_FV_card_map_fun_eq[of S f X S'] strand_size_map_fun_lt(2)[of X f] by simp

lemma LI_unify_measure_lt:
  assumes "Some \<delta> = mgu (Fun f X) t" "FV t \<subseteq> FV\<^sub>s\<^sub>t S"
  shows "(((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>,\<theta>\<^sub>1), (S@snd\<langle>Fun f X\<rangle>#S',\<theta>\<^sub>2)) \<in> measure\<^sub>s\<^sub>t"
proof (cases "\<delta> = Var")
  assume "\<delta> = Var"
  hence "(S@S') \<cdot>\<^sub>s\<^sub>t \<delta> = S@S'" by blast
  thus ?thesis using strand_FV_card_rm_fun_le[of S S' f X] by auto
next
  assume "\<delta> \<noteq> Var"
  then obtain v where "v \<in> FV (Fun f X) \<union> FV t" "elim \<delta> v"
    using mgu_eliminates[OF assms(1)[symmetric]] by metis
  hence v_in: "v \<in> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" using assms(2) by auto
  
  have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV (Fun f X) \<union> FV\<^sub>s\<^sub>t S"
    using assms(2) mgu_vars_bounded[OF assms(1)[symmetric]] by auto
  hence img_bound: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" by auto

  have finite_FV: "finite (FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))" by auto

  have "v \<notin> FV\<^sub>s\<^sub>t ((S@snd\<langle>Fun f X\<rangle>#S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
    using strand_FV_subst_subset_if_elim[OF \<open>elim \<delta> v\<close>] v_in by metis
  hence v_not_in: "v \<notin> FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" by auto
  
  have "FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
    using strand_subst_FV_bounded_if_img_bounded[OF img_bound] by simp
  hence "FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subset> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" using v_in v_not_in by blast
  hence "card (FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)) < card (FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S'))"
    using psubset_card_mono[OF finite_FV] by simp
  thus ?thesis by auto
qed

lemma LI_equality_measure_lt:
  assumes "Some \<delta> = mgu t t'"
  shows "(((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>,\<theta>\<^sub>1), (S@t \<doteq> t'#S',\<theta>\<^sub>2)) \<in> measure\<^sub>s\<^sub>t"
proof (cases "\<delta> = Var")
  assume "\<delta> = Var"
  hence "(S@S') \<cdot>\<^sub>s\<^sub>t \<delta> = S@S'" by blast
  thus ?thesis using strand_FV_card_rm_eq_le[of S S' t t'] by auto
next
  assume "\<delta> \<noteq> Var"
  then obtain v where "v \<in> FV t \<union> FV t'" "elim \<delta> v"
    using mgu_eliminates[OF assms(1)[symmetric]] by metis
  hence v_in: "v \<in> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" using assms by auto
  
  have "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV t \<union> FV t' \<union> FV\<^sub>s\<^sub>t S"
    using assms mgu_vars_bounded[OF assms(1)[symmetric]] by auto
  hence img_bound: "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" by auto

  have finite_FV: "finite (FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))" by auto

  have "v \<notin> FV\<^sub>s\<^sub>t ((S@t \<doteq> t'#S') \<cdot>\<^sub>s\<^sub>t \<delta>)"
    using strand_FV_subst_subset_if_elim[OF \<open>elim \<delta> v\<close>] v_in by metis
  hence v_not_in: "v \<notin> FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)" by auto
  
  have "FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
    using strand_subst_FV_bounded_if_img_bounded[OF img_bound] by simp
  hence "FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>) \<subset> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" using v_in v_not_in by blast
  hence "card (FV\<^sub>s\<^sub>t ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>)) < card (FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S'))"
    using psubset_card_mono[OF finite_FV] by simp
  thus ?thesis by auto
qed

lemma LI_in_measure: "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto> (S\<^sub>2,\<theta>\<^sub>2) \<Longrightarrow> ((S\<^sub>2,\<theta>\<^sub>2),(S\<^sub>1,\<theta>\<^sub>1)) \<in> measure\<^sub>s\<^sub>t"
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' \<theta>) thus ?case using LI_compose_measure_lt[of S X S'] by metis
next
  case (Unify S f Y \<delta> X S' \<theta>)
  hence "FV (Fun f Y) \<subseteq> FV\<^sub>s\<^sub>t S"
    using FV_snd_rcv_strand_subset(2)[of S] by fastforce
  thus ?case using LI_unify_measure_lt[OF Unify.hyps(3), of S S'] by metis
qed (metis LI_equality_measure_lt)

lemma LI_in_measure_trans: "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>+ (S\<^sub>2,\<theta>\<^sub>2) \<Longrightarrow> ((S\<^sub>2,\<theta>\<^sub>2),(S\<^sub>1,\<theta>\<^sub>1)) \<in> measure\<^sub>s\<^sub>t"
apply (induction rule: trancl.induct, metis surjective_pairing LI_in_measure)
by (metis (no_types, lifting) surjective_pairing LI_in_measure measure\<^sub>s\<^sub>t_trans trans_def)

lemma LI_converse_wellfounded_trans: "wf ((LI_rel\<^sup>+)\<inverse>)"
proof -
  have "(LI_rel\<^sup>+)\<inverse> \<subseteq> measure\<^sub>s\<^sub>t" using LI_in_measure_trans by auto
  thus ?thesis using measure\<^sub>s\<^sub>t_wellfounded wf_subset by metis
qed

lemma LI_acyclic_trans: "acyclic (LI_rel\<^sup>+)"
using wf_acyclic[OF LI_converse_wellfounded_trans] acyclic_converse by metis

lemma LI_acyclic: "acyclic LI_rel"
using LI_acyclic_trans acyclic_subset by (simp add: acyclic_def)

lemma LI_no_infinite_chain: "\<not>(\<exists>f. \<forall>i. f i \<leadsto>\<^sup>+ f (Suc i))"
proof -
  have "\<not>(\<exists>f. \<forall>i. (f (Suc i), f i) \<in> (LI_rel\<^sup>+)\<inverse>)"
    using wf_iff_no_infinite_down_chain LI_converse_wellfounded_trans by metis
  thus ?thesis by simp
qed

lemma LI_unify_finite:
  assumes "finite M"
  shows "finite {((S@snd\<langle>Fun f X\<rangle>#S',\<theta>), ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>,\<theta> \<circ>\<^sub>s \<delta>)) | \<delta> Y. 
                   simple S \<and> Fun f Y \<in> M \<and> Some \<delta> = mgu (Fun f X) (Fun f Y)}"
using assms
proof (induction M rule: finite_induct)
  case (insert m M) thus ?case
  proof (cases m)
    case (Fun g Z)
    let ?a = "\<lambda>\<delta>. ((S@snd\<langle>Fun f X\<rangle>#S',\<theta>), ((S@S') \<cdot>\<^sub>s\<^sub>t \<delta>,\<theta> \<circ>\<^sub>s \<delta>))"
    let ?A = "\<lambda>B. {?a \<delta> | \<delta> Y. simple S \<and> Fun f Y \<in> B \<and> Some \<delta> = mgu (Fun f X) (Fun f Y)}"

    have "?A (insert m M) = (?A M) \<union> (?A {m})" by auto
    moreover have "finite (?A {m})"
    proof (cases "\<exists>\<delta>. Some \<delta> = mgu (Fun f X) (Fun g Z)")
      case True
      then obtain \<delta> where \<delta>: "Some \<delta> = mgu (Fun f X) (Fun g Z)" by blast
      
      have A_m_eq: "\<And>\<delta>'. ?a \<delta>' \<in> ?A {m} \<Longrightarrow> ?a \<delta> = ?a \<delta>'"
      proof -
        fix \<delta>' assume "?a \<delta>' \<in> ?A {m}"
        hence "\<exists>\<sigma>. Some \<sigma> = mgu (Fun f X) (Fun g Z) \<and> ?a \<sigma> = ?a \<delta>'" using \<open>m = Fun g Z\<close> by auto
        thus "?a \<delta> = ?a \<delta>'" by (metis \<delta> option.inject)
      qed

      have "?A {m} = {} \<or> ?A {m} = {?a \<delta>}"
      proof (cases "simple S \<and> ?A {m} \<noteq> {}")
        case True
        hence "simple S" "?A {m} \<noteq> {}" by meson+
        hence "?A {m} = {?a \<delta> | \<delta>. Some \<delta> = mgu (Fun f X) (Fun g Z)}" using \<open>m = Fun g Z\<close> by auto
        hence "?a \<delta> \<in> ?A {m}" using \<delta> by auto
       show ?thesis
        proof (rule ccontr)
          assume "\<not>(?A {m} = {} \<or> ?A {m} = {?a \<delta>})"
          then obtain B where B: "?A {m} = insert (?a \<delta>) B" "?a \<delta> \<notin> B" "B \<noteq> {}"
            using \<open>?A {m} \<noteq> {}\<close> \<open>?a \<delta> \<in> ?A {m}\<close> by (metis (no_types, lifting) Set.set_insert)
          then obtain b where b: "?a \<delta> \<noteq> b" "b \<in> B" by (metis (no_types, lifting) ex_in_conv)
          then obtain \<delta>' where \<delta>': "b = ?a \<delta>'" using B(1) by blast
          moreover have "?a \<delta>' \<in> ?A {m}" using B(1) b(2) \<delta>' by auto
          hence "?a \<delta> = ?a \<delta>'" by (blast dest!: A_m_eq)
          ultimately show False using b(1) by simp
        qed
      qed auto
      thus ?thesis by (metis (no_types, lifting) finite.emptyI finite_insert) 
    next
      case False
      hence "?A {m} = {}" using \<open>m = Fun g Z\<close> by blast
      thus ?thesis by (metis finite.emptyI)
    qed
    ultimately show ?thesis using insert.IH by auto
  qed simp
qed fastforce


subsection {* Lemma: The lazy intruder preserves well-formedness *}
lemma LI_preserves_trm_wf:
  assumes "(S,\<theta>) \<leadsto>\<^sup>* (S',\<theta>')" "\<forall>x \<in> set S. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
  shows "\<forall>x \<in> set S'. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
proof -
  { fix S \<theta> S' \<theta>'
    assume "(S,\<theta>) \<leadsto> (S',\<theta>')" "\<forall>x \<in> set S. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
    hence "\<forall>x \<in> set S'. wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
    proof (induction rule: LI_rel.induct)
      case (Compose S X f S' \<theta>)
      hence "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)"
        and *: "\<And>x. x \<in> set S \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
               "\<And>x. x \<in> set S' \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
        by auto
      hence "\<And>x. x \<in> set X \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m x" unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
      hence "\<And>x. x \<in> set (map Send X) \<Longrightarrow> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p x) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p x)"
        unfolding wf\<^sub>t\<^sub>r\<^sub>m_def by auto
      thus ?case using * by auto
    next
      case (Unify S f Y \<delta> X S' \<theta>)
      have "wf\<^sub>t\<^sub>r\<^sub>m (Fun f X)" "wf\<^sub>t\<^sub>r\<^sub>m (Fun f Y)"
        using Unify.prems(1) Unify.hyps(2) wf_trm_subterm[of _ "Fun f Y"]
        by (simp, force)
      hence "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)" using mgu_wf_trm[OF Unify.hyps(3)[symmetric]] by simp

      { fix s assume "s \<in> set (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>)"
        hence "\<exists>s' \<in> set (S@S'). s = s' \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s') \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')"
          using Unify.prems(1) by auto
        moreover {
          fix s' assume "s = s' \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')" "s' \<in> set (S@S')"
          hence "trm\<^sub>s\<^sub>t\<^sub>p s = trm\<^sub>s\<^sub>t\<^sub>p s' \<cdot> (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \<delta>)"
                "trm_r\<^sub>s\<^sub>t\<^sub>p s = trm_r\<^sub>s\<^sub>t\<^sub>p s' \<cdot> (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \<delta>)"
            by (cases s'; auto)+
          hence "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s)" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)"
            by (simp_all add: wf_trm_subst \<open>\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')\<close>)
        }
        ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)" by auto
      }
      thus ?case by simp
    next
      case (Equality S \<delta> t t' S' \<theta>)
      hence "wf\<^sub>t\<^sub>r\<^sub>m t" "wf\<^sub>t\<^sub>r\<^sub>m t'" by simp_all
      hence "\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)" using mgu_wf_trm[OF Equality.hyps(2)[symmetric]] by simp

      { fix s assume "s \<in> set (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>)"
        hence "\<exists>s' \<in> set (S@S'). s = s' \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta> \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s') \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')"
          using Equality.prems(1) by auto
        moreover {
          fix s' assume "s = s' \<cdot>\<^sub>s\<^sub>t\<^sub>p \<delta>" "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')" "s' \<in> set (S@S')"
          hence "trm\<^sub>s\<^sub>t\<^sub>p s = trm\<^sub>s\<^sub>t\<^sub>p s' \<cdot> (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \<delta>)"
                "trm_r\<^sub>s\<^sub>t\<^sub>p s = trm_r\<^sub>s\<^sub>t\<^sub>p s' \<cdot> (rm_vars (set (bvars\<^sub>s\<^sub>t\<^sub>p s')) \<delta>)"
            by (cases s'; auto)+
          hence "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s)" "wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)"
            by (simp_all add: wf_trm_subst \<open>\<And>v. wf\<^sub>t\<^sub>r\<^sub>m (\<delta> v)\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s')\<close> \<open>wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s')\<close>)
        }
        ultimately have "wf\<^sub>t\<^sub>r\<^sub>m (trm\<^sub>s\<^sub>t\<^sub>p s) \<and> wf\<^sub>t\<^sub>r\<^sub>m (trm_r\<^sub>s\<^sub>t\<^sub>p s)" by auto
      }
      thus ?case by simp
    qed
  }
  with assms show ?thesis by (induction rule: rtrancl_induct2) metis+
qed

lemma LI_preserves_subst_wf_single:
  assumes "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto> (S\<^sub>2,\<theta>\<^sub>2)" "FV\<^sub>s\<^sub>t S\<^sub>1 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>1 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>1"
  and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>1 \<inter> vars\<^sub>s\<^sub>t S\<^sub>1 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>1 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>1 = {}"
  shows "FV\<^sub>s\<^sub>t S\<^sub>2 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>2 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>2"
  and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>2 \<inter> vars\<^sub>s\<^sub>t S\<^sub>2 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>2 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>2 = {}"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' \<theta>)
  { case 1 thus ?case using vars_st_snd_map by auto }
  { case 2 thus ?case using vars_st_snd_map by auto }
  { case 3 thus ?case using vars_st_snd_map by auto }
  { case 4 thus ?case using vars_st_snd_map by auto }
next
  case (Unify S f Y \<delta> X S' \<theta>)
  hence "FV (Fun f Y) \<subseteq> FV\<^sub>s\<^sub>t S" using FV_subset_if_in_strand_ik'[OF trpI] by blast
  hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
    using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]]
    by fastforce

  have "FV\<^sub>s\<^sub>t (S@S') \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" "vars\<^sub>s\<^sub>t (S@S') \<subseteq> vars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" by auto
  hence **: "FV\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
            "vars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> vars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
    using strand_subst_FV_union_bound[of "S@S'" \<delta>]
          strand_subst_vars_union_bound[of "S@S'" \<delta>] *
    by blast+

  have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (fact mgu_gives_wellformed_subst[OF Unify.hyps(3)[symmetric]])
  
  { case 1
    have "bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
      using bvars_subst_ident[of "S@S'" \<delta>] by auto
    thus ?case using 1 ** by blast
  }
  { case 2
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" using * by blast+
    thus ?case by (metis wf_subst_compose[OF \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>])
  }
  { case 3
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" using ** by blast
    moreover have "\<And>v. v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> v \<in> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" using * by blast
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> FV\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}"
      using mgu_eliminates_dom[OF Unify.hyps(3)[symmetric],
                THEN strand_FV_subst_subset_if_elim, of _ "S@snd\<langle>Fun f X\<rangle>#S'"]
      unfolding elim_def by auto
    moreover have "bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
      using bvars_subst_ident[of "S@S'" \<delta>] by auto
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" using 3(1) * by blast
    ultimately show ?case
      using ** * subst_dom_comp_subset[of \<theta> \<delta>] vars\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>t[of "S@S' \<cdot>\<^sub>s\<^sub>t \<delta>"]
      by blast
  }
  { case 4
    have ***: "bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
      using bvars_subst_ident[of "S@S'" \<delta>] by auto
    hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" using 4(1) * by blast
    thus ?case using subst_img_comp_subset[of \<theta> \<delta>] 4(4) *** by blast
  }
next
  case (Equality S \<delta> t t' S' \<theta>)
  hence *: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
    using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]]
    by fastforce

  have "FV\<^sub>s\<^sub>t (S@S') \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" "vars\<^sub>s\<^sub>t (S@S') \<subseteq> vars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" by auto
  hence **: "FV\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
            "vars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<subseteq> vars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
    using strand_subst_FV_union_bound[of "S@S'" \<delta>]
          strand_subst_vars_union_bound[of "S@S'" \<delta>] *
    by blast+

  have "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>" by (fact mgu_gives_wellformed_subst[OF Equality.hyps(2)[symmetric]])
  
  { case 1
    have "bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
      using bvars_subst_ident[of "S@S'" \<delta>] by auto
    thus ?case using 1 ** by blast
  }
  { case 2
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" using * by blast+
    thus ?case by (metis wf_subst_compose[OF \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<close> \<open>wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>\<close>])
  }
  { case 3
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" using ** by blast
    moreover have "\<And>v. v \<in> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<Longrightarrow> v \<in> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" using * by blast
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> FV\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}"
      using mgu_eliminates_dom[OF Equality.hyps(2)[symmetric],
                THEN strand_FV_subst_subset_if_elim, of _ "S@t \<doteq> t'#S'"]
      unfolding elim_def by auto
    moreover have "bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
      using bvars_subst_ident[of "S@S'" \<delta>] by auto
    hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" using 3(1) * by blast
    ultimately show ?case
      using ** * subst_dom_comp_subset[of \<theta> \<delta>] vars\<^sub>s\<^sub>t_is_FV\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>t[of "S@S' \<cdot>\<^sub>s\<^sub>t \<delta>"]
      by blast
  }
  { case 4
    have ***: "bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = bvars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
      using bvars_subst_ident[of "S@S'" \<delta>] by auto
    hence "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<inter> bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}" using 4(1) * by blast
    thus ?case using subst_img_comp_subset[of \<theta> \<delta>] 4(4) *** by blast
  }
qed

lemma LI_preserves_subst_wf:
  assumes "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2)" "FV\<^sub>s\<^sub>t S\<^sub>1 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>1 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>1"
  and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>1 \<inter> vars\<^sub>s\<^sub>t S\<^sub>1 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>1 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>1 = {}"
  shows "FV\<^sub>s\<^sub>t S\<^sub>2 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>2 = {}" "wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>2"
  and "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>2 \<inter> vars\<^sub>s\<^sub>t S\<^sub>2 = {}" "FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>\<^sub>2 \<inter> bvars\<^sub>s\<^sub>t S\<^sub>2 = {}"
using assms
proof (induction S\<^sub>2 \<theta>\<^sub>2 rule: rtrancl_induct2)
  case (step S\<^sub>i \<theta>\<^sub>i S\<^sub>j \<theta>\<^sub>j)
  { case 1 thus ?case using LI_preserves_subst_wf_single[OF \<open>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j)\<close>] step.IH by metis }
  { case 2 thus ?case using LI_preserves_subst_wf_single[OF \<open>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j)\<close>] step.IH by metis }
  { case 3 thus ?case using LI_preserves_subst_wf_single[OF \<open>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j)\<close>] step.IH by metis }
  { case 4 thus ?case using LI_preserves_subst_wf_single[OF \<open>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j)\<close>] step.IH by metis }
qed metis

lemma LI_preserves_wellformedness:
  "\<lbrakk>(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2); wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<rbrakk> \<Longrightarrow> wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>2 \<theta>\<^sub>2"
proof -
  assume "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2)"

  have *: "\<And>S\<^sub>i \<theta>\<^sub>i S\<^sub>j \<theta>\<^sub>j. \<lbrakk>(S\<^sub>i, \<theta>\<^sub>i) \<leadsto> (S\<^sub>j, \<theta>\<^sub>j); wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>i \<theta>\<^sub>i\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t {} S\<^sub>j"
  proof -
    fix S\<^sub>i \<theta>\<^sub>i S\<^sub>j \<theta>\<^sub>j show "\<lbrakk>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j); wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>i \<theta>\<^sub>i\<rbrakk> \<Longrightarrow> wf\<^sub>s\<^sub>t {} S\<^sub>j"
    proof (induction rule: LI_rel.induct)
      case (Unify S f Y \<delta> X S' \<theta>)
      have "FV (Fun f X) \<union> FV (Fun f Y) \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" using Unify.hyps(2) by force
      hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
        using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by (metis subset_trans)
      hence "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S') = {}"
        using Unify.prems unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by blast
      thus ?case
        using wf_unify[OF _ trpI[OF Unify.hyps(2)] MGU_is_Unifier[OF mgu_gives_MGU], of "{}",
                       OF _ Unify.hyps(3)[symmetric], of S'] Unify.prems(1)
        by auto
    next
      case (Equality S \<delta> t t' S' \<theta>)
      have "FV t \<union> FV t' \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" using Equality.hyps(2) by force
      hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
        using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by (metis subset_trans)
      hence "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t (S@t \<doteq> t'#S') = {}"
        using Equality.prems unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by blast
      thus ?case
        using wf_equality[OF _ Equality.hyps(2)[symmetric], of "{}" S S'] Equality.prems(1)
        by auto
    qed (metis wf_send_compose wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def)
  qed

  from \<open>(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2)\<close> show "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1 \<Longrightarrow> wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>2 \<theta>\<^sub>2"
  proof (induction rule: rtrancl_induct2)
    case (step S\<^sub>i \<theta>\<^sub>i S\<^sub>j \<theta>\<^sub>j) thus ?case
      using LI_preserves_subst_wf_single[OF \<open>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j)\<close>] *[OF \<open>(S\<^sub>i,\<theta>\<^sub>i) \<leadsto> (S\<^sub>j,\<theta>\<^sub>j)\<close>]
      by force
  qed simp
qed


subsection {* Theorem: Soundness of the lazy intruder *}
lemma LI_soundness_single:
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1" "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto> (S\<^sub>2,\<theta>\<^sub>2)" "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2,\<theta>\<^sub>2\<rangle>"
  shows "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1,\<theta>\<^sub>1\<rangle>"
using assms(2,1,3)
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' \<theta>)
  hence *: "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" "\<lbrakk>ik\<^sub>s\<^sub>t S; map Send X\<rbrakk>\<^sub>c \<I>" "\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>"
    unfolding constr_sem_c_def by force+

  have "ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c Fun f X \<cdot> \<I>"
    using *(2) Compose.hyps(2) ComposeC[OF _ Compose.hyps(3), of "map (\<lambda>x. x \<cdot> \<I>) X"]
    unfolding subst_compose_def by force
  thus "\<I> \<Turnstile>\<^sub>c \<langle>S@snd\<langle>Fun f X\<rangle>#S',\<theta>\<rangle>" using *(1,3) \<open>\<I> \<Turnstile>\<^sub>c \<langle>S@map Send X@S',\<theta>\<rangle>\<close> by auto
next
  case (Unify S f Y \<delta> X S' \<theta>)
  have "(\<theta> \<circ>\<^sub>s \<delta>) supports \<I>" "\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>"
    using Unify.prems(2) unfolding constr_sem_c_def by metis+
  then obtain \<sigma> where \<sigma>: "\<theta> \<circ>\<^sub>s \<delta> \<circ>\<^sub>s \<sigma> = \<I>" unfolding subst_compose_def by auto

  have \<theta>fun_id: "Fun f Y \<cdot> \<theta> = Fun f Y" "Fun f X \<cdot> \<theta> = Fun f X"
    using Unify.prems(1) trm_subst_ident[of "Fun f Y" \<theta>]
          FV_subset_if_in_strand_ik[of "Fun f Y" S] Unify.hyps(2) trpI[of "Fun f Y" "ik\<^sub>s\<^sub>t S"]
          FV_snd_rcv_strand_subset(2)[of S]
          strand_vars_split(1)[of S "snd\<langle>Fun f X\<rangle>#S'"]
    unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def apply blast
    using Unify.prems(1) trm_subst_ident[of "Fun f X" \<theta>] unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by fastforce
  hence \<theta>\<delta>_disj:
      "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" 
    using trm_subst_disj mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] apply (blast,blast)
    using Unify.prems(1) unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by blast
  hence \<theta>\<delta>_support: "\<theta> supports \<I>" "\<delta> supports \<I>"
    by (simp_all add: subst_support_comp_split[OF \<open>(\<theta> \<circ>\<^sub>s \<delta>) supports \<I>\<close>])

  have "FV (Fun f X) \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')" "FV (Fun f Y) \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
    using Unify.hyps(2) by force+
  hence \<delta>_vars_bound: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@snd\<langle>Fun f X\<rangle>#S')"
    using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] by blast

  have "\<lbrakk>ik\<^sub>s\<^sub>t S; [snd\<langle>Fun f X\<rangle>]\<rbrakk>\<^sub>c \<I>"
  proof -
    from Unify.hyps(2) have "Fun f Y \<cdot> \<I> \<in> ik\<^sub>s\<^sub>t S \<cdot>set \<I>" by blast
    hence "Fun f Y \<cdot> \<I> \<in> ik\<^sub>s\<^sub>t S \<cdot>set \<I>"
      using trp_subst_apply_subset_set[of \<I> "ik\<^sub>s\<^sub>t S"] by blast
    moreover have "Unifier \<delta> (Fun f X) (Fun f Y)"
      by (fact MGU_is_Unifier[OF mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]])
    ultimately have "Fun f X \<cdot> \<I> \<in> ik\<^sub>s\<^sub>t S \<cdot>set \<I>"
      using \<sigma> by (metis \<theta>fun_id subst_comp) 
    thus ?thesis by simp
  qed

  have "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" "\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>"
  proof -
    have "(S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta> = S@S' \<cdot>\<^sub>s\<^sub>t \<delta>" "(S@S') \<cdot>\<^sub>s\<^sub>t \<theta> = S@S'"
    proof -
      have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S') = {}" using Unify.prems(1) by auto
      hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}"
        using \<theta>\<delta>_disj(2) strand_subst_vars_union_bound[of "S@S'" \<delta>] by blast
      thus "(S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta> = S@S' \<cdot>\<^sub>s\<^sub>t \<delta>" "(S@S') \<cdot>\<^sub>s\<^sub>t \<theta> = S@S'"
        using strand_subst_comp \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S') = {}\<close> by (blast,blast)
    qed
    moreover have "Idem \<delta>" by (fact mgu_gives_Idem[OF Unify.hyps(3)[symmetric]])
    moreover have
        "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t (S@S') = {}"
        "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}"
        "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t (S@S') = {}"
      using wf_constr_bvars_disj[OF Unify.prems(1)]
            wf_constr_bvars_disj'[OF Unify.prems(1) \<delta>_vars_bound]
      by auto
    ultimately have "\<lbrakk>{}; S@S'\<rbrakk>\<^sub>c \<I>"
      using \<open>\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>\<close> \<sigma>
            strand_sem_subst[of \<theta> "S@S' \<cdot>\<^sub>s\<^sub>t \<delta>" "{}" "\<delta> \<circ>\<^sub>s \<sigma>"]
            strand_sem_subst'[of \<theta> "S@S'" "{}" "\<delta> \<circ>\<^sub>s \<sigma>"] 
            strand_sem_subst_Idem[of \<delta> "S@S'" "{}" \<sigma>]
      unfolding constr_sem_c_def
      by (metis subst_all_empty comp_assoc)
    thus "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" "\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>" by auto
  qed
  
  show "\<I> \<Turnstile>\<^sub>c \<langle>S@snd\<langle>Fun f X\<rangle>#S',\<theta>\<rangle>"
    using \<theta>\<delta>_support(1) \<open>\<lbrakk>ik\<^sub>s\<^sub>t S; [snd\<langle>Fun f X\<rangle>]\<rbrakk>\<^sub>c \<I>\<close> \<open>\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>\<close> \<open>\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>\<close>
    by auto
next
  case (Equality S \<delta> t t' S' \<theta>)
  have "(\<theta> \<circ>\<^sub>s \<delta>) supports \<I>" "\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>"
    using Equality.prems(2) unfolding constr_sem_c_def by metis+
  then obtain \<sigma> where \<sigma>: "\<theta> \<circ>\<^sub>s \<delta> \<circ>\<^sub>s \<sigma> = \<I>" unfolding subst_compose_def by auto

  have "FV t \<subseteq> vars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" "FV t' \<subseteq> vars\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" by auto
  moreover have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@t \<doteq> t'#S') = {}"
    using Equality.prems(1) unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def by auto
  ultimately have \<theta>fun_id: "t \<cdot> \<theta> = t" "t' \<cdot> \<theta> = t'"
    using trm_subst_ident[of t \<theta>] trm_subst_ident[of t' \<theta>] by auto
  hence \<theta>\<delta>_disj:
      "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> = {}" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> = {}" 
    using trm_subst_disj mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] apply (blast,blast)
    using Equality.prems(1) unfolding wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r_def wf\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t_def by blast
  hence \<theta>\<delta>_support: "\<theta> supports \<I>" "\<delta> supports \<I>"
    by (simp_all add: subst_support_comp_split[OF \<open>(\<theta> \<circ>\<^sub>s \<delta>) supports \<I>\<close>])

  have "FV t \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" "FV t' \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')" by auto
  hence \<delta>_vars_bound: "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t (S@t \<doteq> t'#S')"
    using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by blast

  have "\<lbrakk>ik\<^sub>s\<^sub>t S; [t \<doteq> t']\<rbrakk>\<^sub>c \<I>"
  proof -
    have "t \<cdot> \<delta> = t' \<cdot> \<delta>"
      using MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
      by metis
    hence "t \<cdot> (\<theta> \<circ>\<^sub>s \<delta>) = t' \<cdot> (\<theta> \<circ>\<^sub>s \<delta>)" by (metis \<theta>fun_id subst_comp)
    hence "t \<cdot> \<I> = t' \<cdot> \<I>" by (metis \<sigma> subst_comp) 
    thus ?thesis by simp
  qed

  have "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" "\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>"
  proof -
    have "(S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta> = S@S' \<cdot>\<^sub>s\<^sub>t \<delta>" "(S@S') \<cdot>\<^sub>s\<^sub>t \<theta> = S@S'"
    proof -
      have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S') = {}" using Equality.prems(1) by auto
      hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV\<^sub>s\<^sub>t (S@S') = {}" by blast
      hence "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> FV\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}"
        using \<theta>\<delta>_disj(2) strand_subst_FV_union_bound[of "S@S'" \<delta>] by blast
      thus "(S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) \<cdot>\<^sub>s\<^sub>t \<theta> = S@S' \<cdot>\<^sub>s\<^sub>t \<delta>" "(S@S') \<cdot>\<^sub>s\<^sub>t \<theta> = S@S'"
        using strand_subst_comp \<open>dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<inter> vars\<^sub>s\<^sub>t (S@S') = {}\<close> by (blast,blast)
    qed
    moreover have "Idem \<delta>" by (fact mgu_gives_Idem[OF Equality.hyps(2)[symmetric]])
    moreover have
        "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t (S@S') = {}"
        "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<theta>) \<inter> bvars\<^sub>s\<^sub>t (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>) = {}"
        "(dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta>) \<inter> bvars\<^sub>s\<^sub>t (S@S') = {}"
      using wf_constr_bvars_disj[OF Equality.prems(1)]
            wf_constr_bvars_disj'[OF Equality.prems(1) \<delta>_vars_bound]
      by auto
    ultimately have "\<lbrakk>{}; S@S'\<rbrakk>\<^sub>c \<I>"
      using \<open>\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>\<close> \<sigma>
            strand_sem_subst[of \<theta> "S@S' \<cdot>\<^sub>s\<^sub>t \<delta>" "{}" "\<delta> \<circ>\<^sub>s \<sigma>"]
            strand_sem_subst'[of \<theta> "S@S'" "{}" "\<delta> \<circ>\<^sub>s \<sigma>"] 
            strand_sem_subst_Idem[of \<delta> "S@S'" "{}" \<sigma>]
      unfolding constr_sem_c_def
      by (metis subst_all_empty comp_assoc)
    thus "\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>" "\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>" by auto
  qed
  
  show "\<I> \<Turnstile>\<^sub>c \<langle>S@t \<doteq> t'#S',\<theta>\<rangle>"
    using \<theta>\<delta>_support(1) \<open>\<lbrakk>ik\<^sub>s\<^sub>t S; [t \<doteq> t']\<rbrakk>\<^sub>c \<I>\<close> \<open>\<lbrakk>{}; S\<rbrakk>\<^sub>c \<I>\<close> \<open>\<lbrakk>ik\<^sub>s\<^sub>t S; S'\<rbrakk>\<^sub>c \<I>\<close>
    by auto
qed

theorem LI_soundness:
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1" "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2)" "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>"
  shows "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>"
using assms(2,1,3)
proof (induction S\<^sub>2 \<theta>\<^sub>2 rule: rtrancl_induct2)
  case (step S\<^sub>i \<theta>\<^sub>i S\<^sub>j \<theta>\<^sub>j) thus ?case
    using LI_preserves_wellformedness[OF \<open>(S\<^sub>1, \<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>i, \<theta>\<^sub>i)\<close> \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close>]
          LI_soundness_single[OF _ \<open>(S\<^sub>i, \<theta>\<^sub>i) \<leadsto> (S\<^sub>j, \<theta>\<^sub>j)\<close> \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>j, \<theta>\<^sub>j\<rangle>\<close>]
          step.IH[OF \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close>]
    by metis
qed metis

subsection {* Theorem: Completeness of the lazy intruder *}
lemma LI_completeness_single:
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1" "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>" "\<not>simple S\<^sub>1"
  shows "\<exists>S\<^sub>2 \<theta>\<^sub>2. (S\<^sub>1,\<theta>\<^sub>1) \<leadsto> (S\<^sub>2,\<theta>\<^sub>2) \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>)"
using not_simple_elim[OF \<open>\<not>simple S\<^sub>1\<close>]
proof
  (* In this case S\<^sub>1 isn't simple because it contains an equality constraint,
     so we can simply proceed with the reduction by computing the MGU for the equation *)
  assume "\<exists>S' S'' t t'. S\<^sub>1 = S'@t \<doteq> t'#S'' \<and> simple S'"
  then obtain S t t' S' where S\<^sub>1: "S\<^sub>1 = S@t \<doteq> t'#S'" "simple S" by moura
  hence *: "wf\<^sub>s\<^sub>t {} S" "\<I> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<^sub>1\<rangle>" "\<theta>\<^sub>1 supports \<I>" "t \<cdot> \<I> = t' \<cdot> \<I>" "FV t' \<subseteq> FV\<^sub>s\<^sub>t S"
    using \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close> wf_eq_FV[of "{}" S t t' S']
          FV_snd_rcv_strand_subset(5)[of S]
    by auto

  from * have "Unifier \<I> t t'" by simp
  then obtain \<delta> where \<delta>: "Some \<delta> = mgu t t'" "Idem \<delta>" "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV t \<union> FV t'"
    using mgu_always_unifies mgu_gives_Idem mgu_vars_bounded by metis+
  
  have "\<delta> \<preceq>\<^sub>\<circ> \<I>"
    using mgu_gives_MGU[OF \<delta>(1)[symmetric]]
    by (metis \<open>Unifier \<I> t t'\<close>)
  hence "\<delta> supports \<I>" using subst_support_if_mgt_Idem[OF _ \<delta>(2)] by metis
  hence "(\<theta>\<^sub>1 \<circ>\<^sub>s \<delta>) supports \<I>" using subst_support_comp \<open>\<theta>\<^sub>1 supports \<I>\<close> by metis
  
  have "\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>"
  proof -
    have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S\<^sub>1" using \<delta>(3) S\<^sub>1(1) by auto
    hence "\<lbrakk>{}; S\<^sub>1 \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>"
      using \<open>Idem \<delta>\<close> \<open>\<delta> \<preceq>\<^sub>\<circ> \<I>\<close> \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> strand_sem_subst wf_constr_bvars_disj'(1)[OF assms(1)]
      unfolding Idem_def constr_sem_c_def by (metis (no_types) subst_all_empty comp_assoc)
    thus "\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>" using S\<^sub>1(1) by force
  qed
  moreover have "(S@t \<doteq> t'#S', \<theta>\<^sub>1) \<leadsto> (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>, \<theta>\<^sub>1 \<circ>\<^sub>s \<delta>)"
    using LI_rel.Equality[OF \<open>simple S\<close> \<delta>(1)] S\<^sub>1 by metis
  ultimately show ?thesis using S\<^sub>1(1) \<open>(\<theta>\<^sub>1 \<circ>\<^sub>s \<delta>) supports \<I>\<close> by auto
next
  (* In this case S\<^sub>1 isn't simple because it contains a deduction constraint for a composed term,
     so we must look at how this composed term is derived under the interpretation \<I> *)
  assume "\<exists>S' S'' f X. S\<^sub>1 = S'@snd\<langle>Fun f X\<rangle>#S'' \<and> simple S'"
  with assms obtain S f X S' where S\<^sub>1: "S\<^sub>1 = S@snd\<langle>Fun f X\<rangle>#S'" "simple S"
    using not_simple_elim[OF \<open>\<not>simple S\<^sub>1\<close>] by metis
  hence "wf\<^sub>s\<^sub>t {} S" "\<I> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<^sub>1\<rangle>" "\<theta>\<^sub>1 supports \<I>" using \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close> by auto

  (* Lemma for a common subcase *)
  have fun_sat:
    "(\<And>x. x \<in> set X \<Longrightarrow> ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c x \<cdot> \<I>) \<Longrightarrow> \<I> \<Turnstile>\<^sub>c \<langle>S@(map Send X)@S', \<theta>\<^sub>1\<rangle>"
  proof -
    assume "\<And>x. x \<in> set X \<Longrightarrow> ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c x \<cdot> \<I>"
    hence "\<And>x. x \<in> set X \<Longrightarrow> \<lbrakk>ik\<^sub>s\<^sub>t S; [snd\<langle>x\<rangle>]\<rbrakk>\<^sub>c \<I>" by simp
    hence "\<lbrakk>ik\<^sub>s\<^sub>t S; map Send X\<rbrakk>\<^sub>c \<I>" using \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> strand_sem_snd_map by metis
    moreover have "\<lbrakk>ik\<^sub>s\<^sub>t (S@(map Send X)); S'\<rbrakk>\<^sub>c \<I>" using \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> S\<^sub>1 by auto
    ultimately show ?thesis using \<open>\<I> \<Turnstile>\<^sub>c \<langle>S, \<theta>\<^sub>1\<rangle>\<close> \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> by force
  qed

  from S\<^sub>1 \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> have "ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c Fun f X \<cdot> \<I>" by auto
  thus ?thesis
  proof cases
    (* Case 1: \<I>(f(X)) has been derived using the AxiomC rule.*)
    case AxiomC
    hence ex_t: "\<exists>t. t \<in> ik\<^sub>s\<^sub>t S \<and> Fun f X \<cdot> \<I> = t \<cdot> \<I>" by auto
    show ?thesis
    proof (cases "\<forall>Y. Fun f Y \<in> ik\<^sub>s\<^sub>t S \<longrightarrow> Fun f X \<cdot> \<I> \<noteq> Fun f Y \<cdot> \<I>")
      (* Case 1.1: f(X) is equal to a variable in the intruder knowledge under \<I>.
         Hence there must exists a deduction constraint in the simple prefix of the constraint
         in which this variable occurs/"is sent" for the first time. Since this variable itself
         cannot have been derived from the AxiomC rule (because it must be equal under the
         interpretation to f(X), which is by assumption not in the intruder knowledge under \<I>)
         it must be the case that we can derive it using the ComposeC rule. Hence we can apply
         the Compose rule of the lazy intruder to f(X).
         *)
      case True
      have "\<exists>v. Var v \<in> ik\<^sub>s\<^sub>t S \<and> Fun f X \<cdot> \<I> = \<I> v"
      proof -
        obtain t where "t \<in> ik\<^sub>s\<^sub>t S" "Fun f X \<cdot> \<I> = t \<cdot> \<I>" using ex_t by moura
        thus ?thesis
          using \<open>\<forall>Y. Fun f Y \<in> ik\<^sub>s\<^sub>t S \<longrightarrow> Fun f X \<cdot> \<I> \<noteq> Fun f Y \<cdot> \<I>\<close>
          by (cases t) auto
      qed
      hence "\<exists>v \<in> vars2\<^sub>s\<^sub>t S. Fun f X \<cdot> \<I> = \<I> v"
        by (meson vars_subset_if_in_strand_ik2 trpI contra_subsetD trp_refl trp_var_is_FV)
      then obtain v S\<^sub>p\<^sub>r\<^sub>e S\<^sub>s\<^sub>u\<^sub>f
        where S: "S = S\<^sub>p\<^sub>r\<^sub>e@snd\<langle>Var v\<rangle>#S\<^sub>s\<^sub>u\<^sub>f" "Fun f X \<cdot> \<I> = \<I> v"
                 "\<not>(\<exists>w \<in> vars2\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. Fun f X \<cdot> \<I> = \<I> w)"
        using \<open>wf\<^sub>s\<^sub>t {} S\<close> wf_simple_strand_first_snd_var_split[OF _ \<open>simple S\<close>, of "Fun f X" \<I>]
        by auto
      hence "\<forall>w. Var w \<in> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<longrightarrow> \<I> v \<noteq> Var w \<cdot> \<I>" by force
      moreover have "\<forall>Y. Fun f Y \<in> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<longrightarrow> Fun f X \<cdot> \<I> \<noteq> Fun f Y \<cdot> \<I>"
        using \<open>\<forall>Y. Fun f Y \<in> ik\<^sub>s\<^sub>t S \<longrightarrow> Fun f X \<cdot> \<I> \<noteq> Fun f Y \<cdot> \<I>\<close> S(1)
        by (meson contra_subsetD ik_append_subset(1))
      hence "\<forall>g Y. Fun g Y \<in> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<longrightarrow> \<I> v \<noteq> Fun g Y \<cdot> \<I>" using S(2) by simp
      ultimately have "\<forall>t \<in> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e. \<I> v \<noteq> t \<cdot> \<I>" by (metis term.exhaust)
      hence "\<I> v \<notin> (ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e) \<cdot>set \<I>" by auto

      have "ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I> \<turnstile>\<^sub>c \<I> v" using S\<^sub>1(1) S(1) \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> by auto
      hence "ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I> \<turnstile>\<^sub>c Fun f X \<cdot> \<I>" using \<open>Fun f X \<cdot> \<I> = \<I> v\<close> by metis
      hence "length X = arity f" "public f" "\<And>x. x \<in> set X \<Longrightarrow> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I> \<turnstile>\<^sub>c x \<cdot> \<I>"
        using \<open>Fun f X \<cdot> \<I> = \<I> v\<close> \<open>\<I> v \<notin> ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I>\<close>
              intruder_synth.simps[of "ik\<^sub>s\<^sub>t S\<^sub>p\<^sub>r\<^sub>e \<cdot>set \<I>" "\<I> v"]
        by auto
      hence *: "\<And>x. x \<in> set X \<Longrightarrow> ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c x \<cdot> \<I>"
        using S(1) by (auto intro: ideduct_synth_mono)
      hence "\<I> \<Turnstile>\<^sub>c \<langle>S@(map Send X)@S', \<theta>\<^sub>1\<rangle>" by (metis fun_sat)
      moreover have "(S@snd\<langle>Fun f X\<rangle>#S', \<theta>\<^sub>1) \<leadsto> (S@map Send X@S', \<theta>\<^sub>1)"
        by (metis LI_rel.Compose[OF \<open>simple S\<close> \<open>length X = arity f\<close> \<open>public f\<close>])
      ultimately show ?thesis using S\<^sub>1 by auto
    next
      (* Case 1.2: \<I>(f(X)) can be derived from an interpreted composed term in the intruder
         knowledge. Use the Unify rule on this composed term to further reduce the constraint. *)
      case False
      then obtain Y where t: "Fun f Y \<in> ik\<^sub>s\<^sub>t S" "Fun f X \<cdot> \<I> = Fun f Y \<cdot> \<I>"
        by auto
      hence "FV (Fun f Y) \<subseteq> FV\<^sub>s\<^sub>t S\<^sub>1"
        using S\<^sub>1(1) FV_subset_if_in_strand_ik'[OF trpI[OF t(1)]]
              FV_snd_rcv_strand_subset(2)[of S]
        by auto
      from t have "Unifier \<I> (Fun f X) (Fun f Y)" by simp
      then obtain \<delta> where \<delta>:
          "Some \<delta> = mgu (Fun f X) (Fun f Y)" "Idem \<delta>"
          "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV (Fun f X) \<union> FV (Fun f Y)"
        using mgu_always_unifies mgu_gives_Idem mgu_vars_bounded by metis+
      
      have "\<delta> \<preceq>\<^sub>\<circ> \<I>"
        using mgu_gives_MGU[OF \<delta>(1)[symmetric]]
        by (metis \<open>Unifier \<I> (Fun f X) (Fun f Y)\<close>)
      hence "\<delta> supports \<I>" using subst_support_if_mgt_Idem[OF _ \<delta>(2)] by metis
      hence "(\<theta>\<^sub>1 \<circ>\<^sub>s \<delta>) supports \<I>" using subst_support_comp \<open>\<theta>\<^sub>1 supports \<I>\<close> by metis
      
      have "\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>"
      proof -
        have "dom\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<union> FV_img\<^sub>s\<^sub>u\<^sub>b\<^sub>s\<^sub>t \<delta> \<subseteq> FV\<^sub>s\<^sub>t S\<^sub>1"
          using \<delta>(3) S\<^sub>1(1) \<open>FV (Fun f Y) \<subseteq> FV\<^sub>s\<^sub>t S\<^sub>1\<close> by fastforce
        hence "\<lbrakk>{}; S\<^sub>1 \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>"
          using \<open>Idem \<delta>\<close> \<open>\<delta> \<preceq>\<^sub>\<circ> \<I>\<close> \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close> strand_sem_subst
                wf_constr_bvars_disj'(1)[OF assms(1)]
          unfolding Idem_def constr_sem_c_def by (metis (no_types) subst_all_empty comp_assoc)
        thus "\<lbrakk>{}; S@S' \<cdot>\<^sub>s\<^sub>t \<delta>\<rbrakk>\<^sub>c \<I>" using S\<^sub>1(1) by force
      qed
      moreover have "(S@snd\<langle>Fun f X\<rangle>#S', \<theta>\<^sub>1) \<leadsto> (S@S' \<cdot>\<^sub>s\<^sub>t \<delta>, \<theta>\<^sub>1 \<circ>\<^sub>s \<delta>)"
        using LI_rel.Unify[OF \<open>simple S\<close> t(1) \<delta>(1)] S\<^sub>1 by metis
      ultimately show ?thesis using S\<^sub>1(1) \<open>(\<theta>\<^sub>1 \<circ>\<^sub>s \<delta>) supports \<I>\<close> by auto
    qed
  next
    (* Case 2: \<I>(f(X)) has been derived using the ComposeC rule.
       Simply use the Compose rule of the lazy intruder to proceed with the reduction. *)
    case (ComposeC Y g)
    hence "f = g" "length X = arity f" "public f"
      and "\<And>x. x \<in> set X \<Longrightarrow> ik\<^sub>s\<^sub>t S \<cdot>set \<I> \<turnstile>\<^sub>c x \<cdot> \<I>"
      by auto
    hence "\<I> \<Turnstile>\<^sub>c \<langle>S@(map Send X)@S', \<theta>\<^sub>1\<rangle>" using fun_sat by metis
    moreover have "(S\<^sub>1, \<theta>\<^sub>1) \<leadsto> (S@(map Send X)@S', \<theta>\<^sub>1)"
      using S\<^sub>1 LI_rel.Compose[OF \<open>simple S\<close> \<open>length X = arity f\<close> \<open>public f\<close>]
      by metis
    ultimately show ?thesis by metis
  qed
qed

theorem LI_completeness:
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1" "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>"
  shows "\<exists>S\<^sub>2 \<theta>\<^sub>2. (S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2) \<and> simple S\<^sub>2 \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>)"
proof -
  let ?Stuck = "\<lambda>S\<^sub>2 \<theta>\<^sub>2. \<not>(\<exists>S\<^sub>3 \<theta>\<^sub>3. (S\<^sub>2,\<theta>\<^sub>2) \<leadsto> (S\<^sub>3,\<theta>\<^sub>3) \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>3, \<theta>\<^sub>3\<rangle>))"
  let ?SATConfs = "{(x,(S\<^sub>2,\<theta>\<^sub>2)) \<in> reachable LI_rel (S\<^sub>1,\<theta>\<^sub>1). \<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>}"

  have simple_if_stuck:
    "\<And>S\<^sub>2 \<theta>\<^sub>2. \<lbrakk>(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>+ (S\<^sub>2,\<theta>\<^sub>2); \<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>; ?Stuck S\<^sub>2 \<theta>\<^sub>2\<rbrakk> \<Longrightarrow> simple S\<^sub>2"
  proof -
    fix S\<^sub>2 \<theta>\<^sub>2 assume "(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>+ (S\<^sub>2,\<theta>\<^sub>2)" "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>" "?Stuck S\<^sub>2 \<theta>\<^sub>2" show "simple S\<^sub>2"
      apply (rule ccontr)
      using \<open>?Stuck S\<^sub>2 \<theta>\<^sub>2\<close> LI_completeness_single[OF _ \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>\<close>]
            trancl_into_rtrancl[OF \<open>(S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>+ (S\<^sub>2,\<theta>\<^sub>2)\<close>]
            LI_preserves_wellformedness[OF _ \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close>, of S\<^sub>2 \<theta>\<^sub>2]
      by metis
  qed

  show ?thesis
  proof (cases "simple S\<^sub>1")
    case False
    hence "\<exists>S\<^sub>2 \<theta>\<^sub>2. (S\<^sub>1,\<theta>\<^sub>1) \<leadsto> (S\<^sub>2,\<theta>\<^sub>2) \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>)" by (metis LI_completeness_single[OF assms])
    hence base: "\<exists>b. ((S\<^sub>1,\<theta>\<^sub>1),b) \<in> ?SATConfs" using reachable.Base[of "(S\<^sub>1,\<theta>\<^sub>1)" _ LI_rel] by blast
  
    { fix S \<theta> S' \<theta>' assume "((S,\<theta>),(S',\<theta>')) \<in> ?SATConfs\<^sup>+"
      hence "(S,\<theta>) \<leadsto>\<^sup>+ (S',\<theta>') \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S', \<theta>'\<rangle>)" by (induct rule: trancl_induct2) auto
    }
    hence *: "\<And>S \<theta> S' \<theta>'. ((S,\<theta>),(S',\<theta>')) \<in> ?SATConfs\<^sup>+ \<Longrightarrow> (S,\<theta>) \<leadsto>\<^sup>+ (S',\<theta>') \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S', \<theta>'\<rangle>)"
      by blast

    have "\<exists>S\<^sub>2 \<theta>\<^sub>2. ((S\<^sub>1,\<theta>\<^sub>1),(S\<^sub>2,\<theta>\<^sub>2)) \<in> ?SATConfs\<^sup>+ \<and> ?Stuck S\<^sub>2 \<theta>\<^sub>2"
    proof (rule ccontr)
      assume "\<not>(\<exists>S\<^sub>2 \<theta>\<^sub>2. ((S\<^sub>1,\<theta>\<^sub>1),(S\<^sub>2,\<theta>\<^sub>2)) \<in> ?SATConfs\<^sup>+ \<and> ?Stuck S\<^sub>2 \<theta>\<^sub>2)"
      hence sat_not_stuck: "\<And>S\<^sub>2 \<theta>\<^sub>2. ((S\<^sub>1,\<theta>\<^sub>1),(S\<^sub>2,\<theta>\<^sub>2)) \<in> ?SATConfs\<^sup>+ \<Longrightarrow> \<not>?Stuck S\<^sub>2 \<theta>\<^sub>2" by blast
  
      { fix a assume a: "((S\<^sub>1,\<theta>\<^sub>1),a) \<in> ?SATConfs\<^sup>+"
        { fix S\<^sub>2 \<theta>\<^sub>2 assume in_sat: "((S\<^sub>1,\<theta>\<^sub>1),(S\<^sub>2,\<theta>\<^sub>2)) \<in> ?SATConfs\<^sup>+"
          hence "\<exists>S\<^sub>3 \<theta>\<^sub>3. ((S\<^sub>2,\<theta>\<^sub>2),(S\<^sub>3,\<theta>\<^sub>3)) \<in> ?SATConfs" using * sat_not_stuck by blast
          hence "\<exists>S\<^sub>3 \<theta>\<^sub>3. (S\<^sub>2,\<theta>\<^sub>2) \<leadsto> (S\<^sub>3,\<theta>\<^sub>3) \<and> ((S\<^sub>1,\<theta>\<^sub>1),(S\<^sub>3,\<theta>\<^sub>3)) \<in> ?SATConfs\<^sup>+"
            using trancl_into_trancl[OF in_sat] by blast
        }
        hence "\<And>a. ((S\<^sub>1,\<theta>\<^sub>1),a) \<in> ?SATConfs\<^sup>+ \<Longrightarrow> \<exists>b. a \<leadsto> b \<and> ((S\<^sub>1,\<theta>\<^sub>1),b) \<in> ?SATConfs\<^sup>+" by auto
        hence "\<exists>S' \<theta>'. a \<leadsto> (S',\<theta>') \<and> ((S\<^sub>1,\<theta>\<^sub>1),(S',\<theta>')) \<in> ?SATConfs\<^sup>+" using a by auto
        then obtain S' \<theta>' where S'\<theta>': "a \<leadsto> (S',\<theta>')" "((S\<^sub>1,\<theta>\<^sub>1),(S',\<theta>')) \<in> ?SATConfs\<^sup>+" by auto
        hence "\<I> \<Turnstile>\<^sub>c \<langle>S', \<theta>'\<rangle>" using * by blast
        moreover have "(S\<^sub>1, \<theta>\<^sub>1) \<leadsto>\<^sup>+ a" using a trancl_mono by blast
        ultimately have "(a,(S',\<theta>')) \<in> ?SATConfs" using S'\<theta>'(1) by fastforce
        hence "\<exists>b. (a,b) \<in> ?SATConfs \<and> ((S\<^sub>1,\<theta>\<^sub>1),b) \<in> ?SATConfs\<^sup>+" using S'\<theta>'(2) by blast 
      }
      hence "\<forall>a. ((S\<^sub>1,\<theta>\<^sub>1),a) \<in> ?SATConfs\<^sup>+ \<longrightarrow> (\<exists>b. (a,b) \<in> ?SATConfs)" by blast
      hence "\<exists>f. \<forall>i::nat. (f i, f (Suc i)) \<in> ?SATConfs"
        using infinite_chain_intro'[OF base] by blast
      moreover have "?SATConfs \<subseteq> LI_rel\<^sup>+" by auto
      hence "\<not>(\<exists>f. \<forall>i::nat. (f i, f (Suc i)) \<in> ?SATConfs)"
        using LI_no_infinite_chain infinite_chain_mono by blast
      ultimately show False by auto
    qed
    hence "\<exists>S\<^sub>2 \<theta>\<^sub>2. (S\<^sub>1, \<theta>\<^sub>1) \<leadsto>\<^sup>+ (S\<^sub>2, \<theta>\<^sub>2) \<and> simple S\<^sub>2 \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>)" using simple_if_stuck * by blast
    thus ?thesis by (meson trancl_into_rtrancl)
  qed (blast intro: \<open>\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle>\<close>)
qed


subsection {* Soundness and completeness as a single theorem *}
corollary LI_soundness_and_completeness:
  assumes "wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1"
  shows "\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>1, \<theta>\<^sub>1\<rangle> \<longleftrightarrow> (\<exists>S\<^sub>2 \<theta>\<^sub>2. (S\<^sub>1,\<theta>\<^sub>1) \<leadsto>\<^sup>* (S\<^sub>2,\<theta>\<^sub>2) \<and> simple S\<^sub>2 \<and> (\<I> \<Turnstile>\<^sub>c \<langle>S\<^sub>2, \<theta>\<^sub>2\<rangle>))"
using LI_soundness[OF \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close>] LI_completeness[OF \<open>wf\<^sub>c\<^sub>o\<^sub>n\<^sub>s\<^sub>t\<^sub>r S\<^sub>1 \<theta>\<^sub>1\<close>] by metis

end

end
