Theory EPathHintikka

section ‹Escape path formulas are Hintikka›

theory EPathHintikka imports Hintikka ProverLemmas begin

text ‹In this theory, we show that the formulas in the sequents on a saturated escape path in a
  proof tree form a Hintikka set.
  This is a crucial part of our completeness proof.›

subsection ‹Definitions›
text ‹In this section we define a few concepts that make the following proofs easier to read.›

text ‹‹pseq› is the sequent in a node.›
definition pseq :: ‹state × rule ⇒ sequent› where
  ‹pseq z = snd (fst z)›

text ‹‹ptms› is the list of terms in a node.›
definition ptms :: ‹state × rule ⇒ tm list› where
  ‹ptms z = fst (fst z)›

subsection ‹Facts about streams›

text ‹Escape paths are infinite, so if you drop the first ‹n› nodes, you are still on the path.›
lemma epath_sdrop: ‹epath steps ⟹ epath (sdrop n steps)›
  by (induct n) (auto elim: epath.cases)

text ‹Dropping the first ‹n› elements of a stream can only reduce the set of elements in the stream.›
lemma sset_sdrop: ‹sset (sdrop n s) ⊆ sset s›
proof (induct n arbitrary: s)
  case (Suc n)
  then show ?case
    by (metis in_mono sdrop_simps(2) stl_sset subsetI)
qed simp

subsection  ‹Transformation of states on an escape path›
text ‹We need to prove some lemmas about how the states of an escape path are connected.›

text ‹Since escape paths are well-formed, the eff relation holds between the nodes on the path.›
lemma epath_eff:
  assumes ‹epath steps› ‹eff (snd (shd steps)) (fst (shd steps)) ss›
  shows ‹fst (shd (stl steps)) |∈| ss›
  using assms by (metis (mono_tags, lifting) epath.simps eff_def)

text ‹The list of terms in a state contains the terms of the current sequent and the terms from the
  previous state.›
lemma effect_tms:
  assumes ‹(B, z') |∈| effect r (A, z)›
  shows ‹B = remdups (A @ subterms z @ subterms z')›
  using assms by (smt (verit, best) effect.simps fempty_iff fimageE prod.simps(1))

text ‹The two previous lemmas can be combined into a single lemma.›
lemma epath_effect:
  assumes ‹epath steps› ‹shd steps = ((A, z), r)›
  shows ‹∃B z' r'. (B, z') |∈| effect r (A, z) ∧ shd (stl steps) = ((B, z'), r') ∧
          (B = remdups (A @ subterms z @ subterms z'))›
  using assms epath_eff effect_tms
  by (metis (mono_tags, lifting) eff_def fst_conv prod.collapse snd_conv)

text ‹The list of terms in the next state on an escape path contains the terms in the current state
  plus the terms from the next state.›
lemma epath_stl_ptms:
  assumes ‹epath steps›
  shows ‹ptms (shd (stl steps)) = remdups (ptms (shd steps) @
    subterms (pseq (shd steps)) @ subterms (pseq (shd (stl steps))))›
  using assms epath_effect
  by (metis (mono_tags) eff_def effect_tms epath_eff pseq_def ptms_def surjective_pairing)

text ‹The list of terms never decreases on an escape path.›
lemma epath_sdrop_ptms:
  assumes ‹epath steps›
  shows ‹set (ptms (shd steps)) ⊆ set (ptms (shd (sdrop n steps)))›
  using assms
proof (induct n)
  case (Suc n)
  then have ‹epath (sdrop n steps)›
    using epath_sdrop by blast
  then show ?case
    using Suc epath_stl_ptms by fastforce
qed simp

subsection ‹Preservation of formulas on escape paths›

text ‹If a property will eventually hold on a path, there is some index from which it begins to
  hold, and before which it does not hold.›
lemma ev_prefix_sdrop:
  assumes ‹ev (holds P) xs›
  shows ‹∃n. list_all (not P) (stake n xs) ∧ holds P (sdrop n xs)›
  using assms
proof (induct xs)
  case (base xs)
  then show ?case
    by (metis list.pred_inject(1) sdrop.simps(1) stake.simps(1))
next
  case (step xs)
  then show ?case
    by (metis holds.elims(1) list.pred_inject(2) list_all_simps(2) sdrop.simps(1-2) stake.simps(1-2))
qed

text ‹More specifically, the path will consists of a prefix and a suffix for which the property
  does not hold and does hold, respectively.›
lemma ev_prefix:
  assumes ‹ev (holds P) xs›
  shows ‹∃pre suf. list_all (not P) pre ∧ holds P suf ∧ xs = pre @- suf›
  using assms ev_prefix_sdrop by (metis stake_sdrop)

text ‹All rules are always enabled, so they are also always enabled at specific steps.›
lemma always_enabledAtStep: ‹enabledAtStep r xs›
  by (simp add: RuleSystem_Defs.enabled_def eff_def)

text ‹If a formula is in the sequent in the first state of an escape path and none of the rule
  applications in some prefix of the path affect that formula, the formula will still be in the
  sequent after that prefix.›
lemma epath_preserves_unaffected:
  assumes ‹p ∈ set (pseq (shd steps))› and ‹epath steps› and ‹steps = pre @- suf› and
    ‹list_all (not (λstep. affects (snd step) p)) pre›
  shows ‹p ∈ set (pseq (shd suf))›
  using assms
proof (induct pre arbitrary: steps)
  case Nil
  then show ?case
    by simp
next
  case (Cons q pre)
  from this(3) show ?case
  proof cases
    case (epath sl)
    from this(2-4) show ?thesis
      using Cons(1-2, 4-5) effect_preserves_unaffected unfolding eff_def pseq_def list_all_def
      by (metis (no_types, lifting) list.sel(1) list.set_intros(1-2) prod.exhaust_sel
          shift.simps(2) shift_simps(1) stream.sel(2))
  qed
qed

subsection ‹Formulas on an escape path form a Hintikka set›

text ‹This definition captures the set of formulas on an entire path›
definition ‹tree_fms steps ≡ ⋃ss ∈ sset steps. set (pseq ss)›

text ‹The sequent at the head of a path is in the set of formulas on that path›
lemma pseq_in_tree_fms: ‹⟦x ∈ sset steps; p ∈ set (pseq x)⟧ ⟹ p ∈ tree_fms steps›
  using pseq_def tree_fms_def by blast

text ‹If a formula is in the set of formulas on a path, there is some index on the path where that
  formula can be found in the sequent.›
lemma tree_fms_in_pseq: ‹p ∈ tree_fms steps ⟹ ∃n. p ∈ set (pseq (steps !! n))›
  unfolding pseq_def tree_fms_def using sset_range[of steps] by simp

text ‹If a path is saturated, so is any suffix of that path (since saturation is defined in terms of
  the always operator).›
lemma Saturated_sdrop: ‹Saturated steps ⟹ Saturated (sdrop n steps)›
  by (simp add: RuleSystem_Defs.Saturated_def alw_iff_sdrop saturated_def)

text ‹This is an abbreviation that determines whether a given rule is applied in a given state.›
abbreviation ‹is_rule r step ≡ snd step = r›

text ‹If a path is saturated, it is always possible to find a state in which a given rule is applied.›
lemma Saturated_ev_rule:
  assumes ‹Saturated steps›
  shows ‹ev (holds (is_rule r)) (sdrop n steps)›
proof -
  have ‹Saturated (sdrop n steps)›
    using ‹Saturated steps› Saturated_sdrop by fast
  moreover have ‹r ∈ Prover.R›
    by (metis rules_repeat snth_sset)
  ultimately have ‹saturated r (sdrop n steps)›
    unfolding Saturated_def by fast
  then show ?thesis
    unfolding saturated_def using always_enabledAtStep holds.elims(3) by blast
qed

text ‹On an escape path, the sequent is never an axiom (since that would end the branch, and escape
  paths are infinitely long).›
lemma epath_never_branchDone:
  assumes ‹epath steps›
  shows ‹alw (holds (not (branchDone o pseq))) steps›
proof (rule ccontr)
  assume ‹¬ ?thesis›
  then have ‹ev (holds (branchDone o pseq)) steps›
    by (simp add: alw_iff_sdrop ev_iff_sdrop)
  then obtain n where n: ‹holds (branchDone o pseq) (sdrop n steps)›
    using sdrop_wait by blast
  let ?suf = ‹sdrop n steps›
  have ‹∀r A. effect r (A, pseq (shd ?suf)) = {||}›
    unfolding effect_def using n by simp
  moreover have ‹epath ?suf›
    using ‹epath steps› epath_sdrop by blast
  then have ‹∀r A. ∃z' r'. z' |∈| effect r (A, pseq (shd ?suf)) ∧ shd (stl ?suf) = (z', r')›
    using epath_effect by (metis calculation prod.exhaust_sel pseq_def)
  ultimately show False
    by blast
qed

text ‹Finally we arrive at the main result of this theory:
  The set of formulas on a saturated escape path form a Hintikka set.

  The proof basically says that, given a formula, we can find some index into the path where a rule
  is applied to decompose that formula into the parts needed for the Hintikka set.
  The lemmas above are used to guarantee that the formula does not disappear (and that the branch
  does not end) before the rule is applied, and that the correct formulas are generated by the
  effect function when the rule is finally applied.
  For Beta rules, only one of the constituent formulas need to be on the path, since the path runs
  along only one of the two branches.
  For Gamma and Delta rules, the construction of the list of terms in each state guarantees that
  the formulas are instantiated with terms in the Hintikka set.›
lemma escape_path_Hintikka:
  assumes ‹epath steps› and ‹Saturated steps›
  shows ‹Hintikka (tree_fms steps)›
    (is ‹Hintikka ?H›)
proof
  fix n ts
  assume pre: ‹Pre n ts ∈ ?H›
  then obtain m where m: ‹Pre n ts ∈ set (pseq (shd (sdrop m steps)))›
    using tree_fms_in_pseq by auto

  show ‹Neg (Pre n ts) ∉ ?H›
  proof
    assume ‹Neg (Pre n ts) ∈ ?H›
    then obtain k where k: ‹Neg (Pre n ts) ∈ set (pseq (shd (sdrop k steps)))›
      using tree_fms_in_pseq by auto

    let ?pre = ‹stake (m + k) steps›
    let ?suf = ‹sdrop (m + k) steps›

    have
      1: ‹¬ affects r (Pre n ts)› and
      2: ‹¬ affects r (Neg (Pre n ts))› for r
      unfolding affects_def by (cases r, simp_all)+

    have ‹list_all (not (λstep. affects (snd step) (Pre n ts))) ?pre›
      unfolding list_all_def using 1 by (induct ?pre) simp_all
    then have p: ‹Pre n ts ∈ set (pseq (shd ?suf))›
      using ‹epath steps› epath_preserves_unaffected m epath_sdrop
      by (metis (no_types, lifting) list.pred_mono_strong list_all_append
          sdrop_add stake_add stake_sdrop)

    have ‹list_all (not (λstep. affects (snd step) (Neg (Pre n ts)))) ?pre›
      unfolding list_all_def using 2 by (induct ?pre) simp_all
    then have np: ‹Neg (Pre n ts) ∈ set (pseq (shd ?suf))›
      using ‹epath steps› epath_preserves_unaffected k epath_sdrop
      by (smt (verit, best) add.commute list.pred_mono_strong list_all_append sdrop_add
          stake_add stake_sdrop)

    have ‹holds (branchDone o pseq) ?suf›
      using p np branchDone_contradiction by auto
    moreover have ‹¬ holds (branchDone o pseq) ?suf›
      using ‹epath steps› epath_never_branchDone by (simp add: alw_iff_sdrop)
    ultimately show False
      by blast
  qed
next
  fix p q
  assume ‹Dis p q ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = AlphaDis
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹p ∈ set z'› ‹q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce+

  then show ‹p ∈ ?H ∧ q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Imp p q ∈ tree_fms steps› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = AlphaImp
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹Neg p ∈ set z'› ‹q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce+

  then show ‹Neg p ∈ ?H ∧ q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Neg (Con p q) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = AlphaCon
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹Neg p ∈ set z'› ‹Neg q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce+

  then show ‹Neg p ∈ ?H ∧ Neg q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Con p q ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = BetaCon
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately consider ‹p ∈ set z'› | ‹q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹p ∈ ?H ∨ q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Neg (Imp p q) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = BetaImp
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately consider ‹p ∈ set z'› | ‹Neg q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹p ∈ ?H ∨ Neg q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p q
  assume ‹Neg (Dis p q) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = BetaDis
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately consider ‹Neg p ∈ set z'› | ‹Neg q ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹Neg p ∈ ?H ∨ Neg q ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, opaque_lifting) Un_iff fst_conv pseq_def shd_sset snd_conv sset_sdrop
        sset_shift stl_sset subset_eq)
next
  fix p
  assume ‹Exi p ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto

  let ?r = GammaExi

  show ‹∀t ∈ terms ?H. sub 0 t p ∈ ?H›
  proof
    fix t
    assume t: ‹t ∈ terms ?H›
    show ‹sub 0 t p ∈ ?H›
    proof -
      have ‹∃m. t ∈ set (subterms (pseq (shd (sdrop m steps))))›
      proof (cases ‹(⋃f ∈ ?H. set (subtermFm f)) = {}›)
        case True
        moreover have ‹∀p ∈ set (pseq (shd steps)). p ∈ ?H›
          unfolding tree_fms_def by (metis pseq_in_tree_fms shd_sset tree_fms_def)
        ultimately have ‹∀p ∈ set (pseq (shd steps)). subtermFm p = []›
          by simp
        then have ‹concat (map subtermFm (pseq (shd steps))) = []›
          by (induct ‹pseq (shd steps)›) simp_all
        then have ‹subterms (pseq (shd steps)) = [Fun 0 []]›
          unfolding subterms_def by (metis list.simps(4) remdups_eq_nil_iff)
        then show ?thesis
          using True t unfolding terms_def
          by (metis empty_iff insert_iff list.set_intros(1) sdrop.simps(1))
      next
        case False
        then obtain pt where pt: ‹t ∈ set (subtermFm pt)› ‹pt ∈ ?H›
          using t unfolding terms_def by (metis (no_types, lifting) UN_E)
        then obtain m where m: ‹pt ∈ set (pseq (shd (sdrop m steps)))›
          using tree_fms_in_pseq by auto
        then show ?thesis
          using pt(1) set_subterms by fastforce
      qed
      then obtain m where ‹t ∈ set (subterms (pseq (shd (sdrop m steps))))›
        by blast
      then have ‹t ∈ set (ptms (shd (stl (sdrop m steps))))›
        using epath_stl_ptms epath_sdrop ‹epath steps›
        by (metis (no_types, opaque_lifting) Un_iff set_append set_remdups)
      moreover have ‹epath (stl (sdrop m steps))›
        using epath_sdrop ‹epath steps› by (meson epath.cases)
      ultimately have ‹∀k ≥ m. t ∈ set (ptms (shd (stl (sdrop k steps))))›
        using epath_sdrop_ptms by (metis (no_types, lifting) le_Suc_ex sdrop_add sdrop_stl subsetD)
      then have above: ‹∀k > m. t ∈ set (ptms (shd (sdrop k steps)))›
        by (metis Nat.lessE less_irrefl_nat less_trans_Suc linorder_not_less sdrop_simps(2))

      let ?pre = ‹stake (n + m + 1) steps›
      let ?suf = ‹sdrop (n + m + 1) steps›

      have *: ‹¬ affects r ?f› for r
        unfolding affects_def by (cases r, simp_all)+

      have ‹ev (holds (is_rule ?r)) ?suf›
        using ‹Saturated steps› Saturated_ev_rule by blast
      then obtain pre suf k where
        pre: ‹list_all (not (is_rule ?r)) pre› and
        suf: ‹holds (is_rule ?r) suf› and
        ori: ‹pre = stake k ?suf› ‹suf = sdrop k ?suf›
        using ev_prefix_sdrop by blast

      have k: ‹∃k > m. suf = sdrop k steps›
        using ori by (meson le_add2 less_add_one order_le_less_trans sdrop_add trans_less_add1)

      have ‹list_all (not (λstep. affects (snd step) ?f)) ?pre›
        unfolding list_all_def using * by (induct ?pre) simp_all
      then have ‹?f ∈ set (pseq (shd ?suf))›
        using ‹epath steps› epath_preserves_unaffected n epath_sdrop
        by (metis (no_types, lifting) list.pred_mono_strong list_all_append
            sdrop_add stake_add stake_sdrop)
      then have ‹?f ∈ set (pseq (shd suf))›
        using ‹epath steps› epath_preserves_unaffected n epath_sdrop * ori
        by (metis (no_types, lifting) list.pred_mono_strong pre stake_sdrop)
      moreover have ‹epath suf›
        using ‹epath steps› epath_sdrop ori by blast
      then obtain B z' r' where
        z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))›
        ‹shd (stl suf) = ((B, z'), r')›
        using suf epath_effect unfolding pseq_def ptms_def
        by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)

      moreover have ‹t ∈ set (ptms (shd suf))›
        using above k by (meson le_add2 less_add_one order_le_less_trans)
      ultimately have ‹sub 0 t p ∈ set z'›
        using parts_in_effect[where A=‹ptms (shd suf)›] unfolding parts_def by fastforce
      then show ?thesis
        using k pseq_in_tree_fms z'(2)
        by (metis Pair_inject in_mono prod.collapse pseq_def shd_sset sset_sdrop stl_sset)
    qed
  qed
next
  fix p
  assume ‹Neg (Uni p) ∈ ?H› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto

  let ?r = GammaUni

  show ‹∀t ∈ terms ?H. Neg (sub 0 t p) ∈ ?H›
  proof
    fix t
    assume t: ‹t ∈ terms ?H›
    show ‹Neg (sub 0 t p) ∈ ?H›
    proof -
      have ‹∃m. t ∈ set (subterms (pseq (shd (sdrop m steps))))›
      proof (cases ‹(⋃f ∈ ?H. set (subtermFm f)) = {}›)
        case True
        moreover have ‹∀p ∈ set (pseq (shd steps)). p ∈ ?H›
          unfolding tree_fms_def by (metis pseq_in_tree_fms shd_sset tree_fms_def)
        ultimately have ‹∀p ∈ set (pseq (shd steps)). subtermFm p = []›
          by simp
        then have ‹concat (map subtermFm (pseq (shd steps))) = []›
          by (induct ‹pseq (shd steps)›) simp_all
        then have ‹subterms (pseq (shd steps)) = [Fun 0 []]›
          unfolding subterms_def by (metis list.simps(4) remdups_eq_nil_iff)
        then show ?thesis
          using True t unfolding terms_def
          by (metis empty_iff insert_iff list.set_intros(1) sdrop.simps(1))
      next
        case False
        then obtain pt where pt: ‹t ∈ set (subtermFm pt)› ‹pt ∈ ?H›
          using t unfolding terms_def by (metis (no_types, lifting) UN_E)
        then obtain m where m: ‹pt ∈ set (pseq (shd (sdrop m steps)))›
          using tree_fms_in_pseq by auto
        then show ?thesis
          using pt(1) set_subterms by fastforce
      qed
      then obtain m where ‹t ∈ set (subterms (pseq (shd (sdrop m steps))))›
        by blast
      then have ‹t ∈ set (ptms (shd (stl (sdrop m steps))))›
        using epath_stl_ptms epath_sdrop ‹epath steps›
        by (metis (no_types, lifting) Un_iff set_append set_remdups)
      moreover have ‹epath (stl (sdrop m steps))›
        using epath_sdrop ‹epath steps› by (meson epath.cases)
      ultimately have ‹∀k ≥ m. t ∈ set (ptms (shd (stl (sdrop k steps))))›
        using epath_sdrop_ptms by (metis (no_types, lifting) le_Suc_ex sdrop_add sdrop_stl subsetD)
      then have above: ‹∀k > m. t ∈ set (ptms (shd (sdrop k steps)))›
        by (metis Nat.lessE less_irrefl_nat less_trans_Suc linorder_not_less sdrop_simps(2))

      let ?pre = ‹stake (n + m + 1) steps›
      let ?suf = ‹sdrop (n + m + 1) steps›

      have *: ‹¬ affects r ?f› for r
        unfolding affects_def by (cases r, simp_all)+

      have ‹ev (holds (is_rule ?r)) ?suf›
        using ‹Saturated steps› Saturated_ev_rule by blast
      then obtain pre suf k where
        pre: ‹list_all (not (is_rule ?r)) pre› and
        suf: ‹holds (is_rule ?r) suf› and
        ori: ‹pre = stake k ?suf› ‹suf = sdrop k ?suf›
        using ev_prefix_sdrop by blast

      have k: ‹∃k > m. suf = sdrop k steps›
        using ori by (meson le_add2 less_add_one order_le_less_trans sdrop_add trans_less_add1)

      have ‹list_all (not (λstep. affects (snd step) ?f)) ?pre›
        unfolding list_all_def using * by (induct ?pre) simp_all
      then have ‹?f ∈ set (pseq (shd ?suf))›
        using ‹epath steps› epath_preserves_unaffected n epath_sdrop
        by (metis (no_types, lifting) list.pred_mono_strong list_all_append
            sdrop_add stake_add stake_sdrop)
      then have ‹?f ∈ set (pseq (shd suf))›
        using ‹epath steps› epath_preserves_unaffected n epath_sdrop * ori
        by (metis (no_types, lifting) list.pred_mono_strong pre stake_sdrop)
      moreover have ‹epath suf›
        using ‹epath steps› epath_sdrop ori by blast
      then obtain B z' r' where
        z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))›
        ‹shd (stl suf) = ((B, z'), r')›
        using suf epath_effect unfolding pseq_def ptms_def
        by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)

      moreover have ‹t ∈ set (ptms (shd suf))›
        using above k by (meson le_add2 less_add_one order_le_less_trans)
      ultimately have ‹Neg (sub 0 t p) ∈ set z'›
        using parts_in_effect[where A=‹ptms (shd suf)›] unfolding parts_def by fastforce
      then show ?thesis
        using k pseq_in_tree_fms z'(2)
        by (metis Pair_inject in_mono prod.collapse pseq_def shd_sset sset_sdrop stl_sset)
    qed
  qed
next
  fix p
  assume ‹Uni p ∈ tree_fms steps› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = DeltaUni
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately obtain C where
    C: ‹set (ptms (shd suf)) ⊆ set C› ‹sub 0 (Fun (generateNew C) []) p ∈ set z'›
    using parts_in_effect[where B=B and z'=‹z'› and z=‹pseq (shd suf)› and r=‹?r› and p=‹Uni p›]
    unfolding parts_def by auto
  then have *: ‹sub 0 (Fun (generateNew C) []) p ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, lifting) Pair_inject Un_iff in_mono prod.collapse pseq_def shd_sset
        sset_sdrop sset_shift stl_sset)
  let ?t = ‹Fun (generateNew C) []›
  show ‹∃t ∈ terms ?H. sub 0 t p ∈ ?H›
  proof (cases ‹?t ∈ set (subtermFm (sub 0 ?t p))›)
    case True
    then have ‹?t ∈ terms ?H›
      unfolding terms_def using * by (metis UN_I empty_iff)
    then show ?thesis
      using * by blast
  next
    case False
    then have ‹sub 0 t p = sub 0 ?t p› for t
      using sub_const_transfer by metis
    moreover have ‹terms ?H ≠ {}›
      unfolding terms_def by simp
    then have ‹∃t. t ∈ terms ?H›
      by blast
    ultimately show ?thesis
      using * by metis
  qed
next
  fix p
  assume ‹Neg (Exi p) ∈ tree_fms steps› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = DeltaExi
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately obtain C where
    C: ‹set (ptms (shd suf)) ⊆ set C› ‹Neg (sub 0 (Fun (generateNew C) []) p) ∈ set z'›
    using parts_in_effect[where B=B and z'=z' and z=‹pseq (shd suf)› and r=‹?r› and p=‹Neg (Exi p)›]
    unfolding parts_def by auto
  then have *: ‹Neg (sub 0 (Fun (generateNew C) []) p) ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, lifting) Pair_inject Un_iff in_mono prod.collapse pseq_def shd_sset
        sset_sdrop sset_shift stl_sset)
  let ?t = ‹Fun (generateNew C) []›
  show ‹∃t ∈ terms ?H. Neg (sub 0 t p) ∈ ?H›
  proof (cases ‹?t ∈ set (subtermFm (Neg (sub 0 ?t p)))›)
    case True
    then have ‹?t ∈ terms ?H›
      unfolding terms_def using * by (metis UN_I empty_iff)
    then show ?thesis
      using * by blast
  next
    case False
    then have ‹Neg (sub 0 t p) = Neg (sub 0 ?t p)› for t
      using sub_const_transfer by (metis subtermFm.simps(7))
    moreover have ‹terms ?H ≠ {}›
      unfolding terms_def by simp
    then have ‹∃t. t ∈ terms ?H›
      by blast
    ultimately show ?thesis
      using * by metis
  qed
next
  fix p
  assume ‹Neg (Neg p) ∈ tree_fms steps› (is ‹?f ∈ ?H›)
  then obtain n where n: ‹?f ∈ set (pseq (shd (sdrop n steps)))›
    using tree_fms_in_pseq by auto
  let ?steps = ‹sdrop n steps›
  let ?r = NegNeg
  have ‹ev (holds (is_rule ?r)) ?steps›
    using ‹Saturated steps› Saturated_ev_rule by blast
  then obtain pre suf where
    pre: ‹list_all (not (is_rule ?r)) pre› and
    suf: ‹holds (is_rule ?r) suf› and
    ori: ‹?steps = pre @- suf›
    using ev_prefix by blast

  have ‹affects r ?f ⟷ r = ?r› for r
    unfolding affects_def by (cases r) simp_all
  then have ‹list_all (not (λstep. affects (snd step) ?f)) pre›
    using pre by simp
  moreover have ‹epath (pre @- suf)›
    using ‹epath steps› epath_sdrop ori by metis
  ultimately have ‹?f ∈ set (pseq (shd suf))›
    using epath_preserves_unaffected n ori by metis

  moreover have ‹epath suf›
    using ‹epath (pre @- suf)› epath_sdrop by (metis alwD alw_iff_sdrop alw_shift)
  then obtain B z' r' where
    z': ‹(B, z') |∈| effect ?r (ptms (shd suf), pseq (shd suf))› ‹shd (stl suf) = ((B, z'), r')›
    using suf epath_effect unfolding pseq_def ptms_def
    by (metis (mono_tags, lifting) holds.elims(2) prod.collapse)
  ultimately have ‹p ∈ set z'›
    using parts_in_effect unfolding parts_def by fastforce

  then show ‹p ∈ ?H›
    using z'(2) ori pseq_in_tree_fms
    by (metis (no_types, lifting) Pair_inject Un_iff in_mono prod.collapse pseq_def shd_sset
        sset_sdrop sset_shift stl_sset)
qed

end