# 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
```