theory Subterm_Criterion
imports
QTRS.QDP_Framework
begin
subsection ‹Projections›
text ‹
A projection @{text "proj_term p t"} maps a term with root symbol @{term "f"}
to its @{term "p f"}-th argument or does not change the term at all (if
@{term "p f"} is not an argument position of @{term "f"}. Variables are not changed.
›
type_synonym 'f proj = "('f × nat) ⇒ nat"
fun proj_term :: "'f proj ⇒ ('f, 'v) term ⇒ ('f, 'v) term" where
"proj_term p (Var x) = Var x"
| "proj_term p (Fun f ts) = (let n = length ts; i = p (f,n) in if i < n
then ts ! i
else Fun f ts)"
lemma proj_term_subst_distr[simp]:
"proj_term π (Fun f ss) ⋅ σ = proj_term π (Fun f ss ⋅ σ)"
by (auto simp: Let_def)
lemma supteq_proj_term: "t ⊵ proj_term p t"
by (cases t) (auto simp: Let_def)
lemma proj_term_subst_apply_term_distrib[simp]:
assumes "is_Fun t"
shows "proj_term p t ⋅ σ = proj_term p (t ⋅ σ)"
using assms by (cases t) (simp_all add: Let_def)
lemma qrstep_proj_term:
fixes p :: "'f proj"
defines pi_def[simp]: "π t ≡ proj_term p t"
assumes "¬ defined R (the (root s))"
and nvar: "∀ (l,r) ∈ R. is_Fun l"
and "(s, t) ∈ qrstep nfs Q R"
shows "(π s, π t) ∈ (qrstep nfs Q R)^="
proof -
from nvar_qrstep_Fun[OF nvar ‹(s, t) ∈ qrstep nfs Q R›]
obtain f ss where s: "s = Fun f ss" by best
from ‹(s, t) ∈ qrstep nfs Q R› have "(Fun f ss, t) ∈ qrstep nfs Q R" by (simp add: s)
from this[unfolded qrstep_iff_rqrstep_or_nrqrstep] show ?thesis
proof
assume "(Fun f ss, t) ∈ rqrstep nfs Q R"
then obtain l r σ where "(l, r) ∈ R" and Fun: "Fun f ss = l ⋅ σ" ..
with nvar
obtain ls where l: "l = Fun f ls" by force
from ‹(l, r) ∈ R› have "defined R (f, num_args s)" by (auto simp: defined_def s Fun l)
with assms show ?thesis by (auto simp: s)
next
assume step: "(Fun f ss, t) ∈ nrqrstep nfs Q R"
from nrqrstep_preserves_root[OF step] obtain ts where t: "t = Fun f ts"
by (cases t, auto)
from nrqrstep_imp_arg_qrsteps[OF step] and nrqrstep_num_args[OF step]
have args: "∀i. (ss ! i, args t ! i) ∈ (qrstep nfs Q R)^="
and num_args: "num_args (Fun f ss) = num_args t" unfolding t by auto
with t have len: "length ts = length ss" by simp
let ?i = "p (f,length ss)"
show ?thesis
proof (cases "?i < length ss")
case True
from args have "(ss ! ?i, args t ! ?i) ∈ (qrstep nfs Q R)^=" by simp
thus ?thesis using len unfolding s t pi_def num_args[symmetric]
unfolding proj_term.simps Let_def unfolding len unfolding if_P[OF True] by simp
next
case False
from ‹(s, t) ∈ qrstep nfs Q R›
show ?thesis unfolding s t pi_def proj_term.simps Let_def len if_not_P[OF False]
by simp
qed
qed
qed
lemma qrsteps_proj_term:
assumes steps: "(s, t) ∈ (qrstep nfs Q R)^*" and ndef: "¬ defined R (the (root s))"
and nvar: "∀ (l,r) ∈ R. is_Fun l"
shows "(proj_term p s, proj_term p t) ∈ (qrstep nfs Q R)^*"
using steps ndef
proof (induct)
case base show ?case by simp
next
case (step u v)
hence seq: "(proj_term p s, proj_term p u) ∈ (qrstep nfs Q R)^*" by simp
note steps = qrsteps_imp_nrqrsteps[OF nvar ndef_applicable_rules[OF ndef] step(1)]
from ndef[unfolded nrqrsteps_preserve_root[OF steps] nrqrsteps_num_args[OF steps]]
have ndef: "¬ defined R (the (root u))" .
from qrstep_proj_term[OF ndef nvar]
and ‹(u, v) ∈ qrstep nfs Q R›
have "(proj_term p u, proj_term p v) ∈ qrstep nfs Q R ∪ Id" by simp
with ‹(proj_term p s, proj_term p u) ∈ (qrstep nfs Q R)^*›
show "(proj_term p s, proj_term p v) ∈ (qrstep nfs Q R)^*" by auto
qed
text ‹
Lhss and rhss of @{text "P"} are nonvariable terms with roots that are
not defined in @{text "R"}. The projections of the removed pairs need
to be in the relation @{term "({⊳} ∪ rstep R)^+"}. The projections of
all other pairs need to be equal. This extended version of the subterm
criterion (where now also identity projections and rewrite steps are
possible) is due to the A3PAT team (TODO: add reference). However,
extending our existing proof, was straight-forward, since internally we
already used exactly this relation, but just did not realize that we could
lift it to the main result.
Extension: For @{text Q}-restricted rewriting, at most a single rewrite-step
is allowed between the projections of the removed pairs.
Moreover, for innermost rewriting, no minimality is required.
Comment: if Q ≠ {} and NF Q ⊆ NF R (usual innermost or more restrictive case) then the restriction
do single rewrite steps is not a real restriction: in fact, not a single rewrite-step can be performed,
because if π(s) ⊵ ⋅ -Q→_R t, then s is not in NF R and thus not in NF Q. Hence, then this DP can immediately
dropped by other criteria like the dependency graph.
if however Q ≠ {} and ¬ NF Q ⊆ NF R, then the condition is required for soundness:
Consider P = {F(f(x)) → F(g(x))}, R = {f(x) → h(i(x)), h(i(x)) → g(x), g(x) → f(x)} and Q = {i(a)}.
We get an infinite minimal chain F(f(a)) -P→ F(g(a)) -R→ F(f(a)) -P→ ...
However, the criterion which allows more than one step would allow do delete the pair as
F(f(x)) -R→ F(h(i(x))) -R→ F(g(x))
›
definition
subterm_criterion_cond ::
"'f proj ⇒ bool ⇒ ('f, 'v) trs ⇒ ('f, 'v) terms ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs ⇒ bool"
where
"subterm_criterion_cond p nfs P Q R D ≡
(∀(l, r)∈P. is_Fun l ∧ is_Fun r ∧ ¬ defined R (the (root r))) ∧
(∀(l, r)∈P - D. proj_term p l = proj_term p r) ∧
(∀(l, r)∈R. is_Fun l) ∧
((Q = {} ∧ (∀(l, r)∈D. (proj_term p l, proj_term p r) ∈ ({⊳} ∪ rstep R)^+)) ∨
(∀(l, r)∈D. (proj_term p l, proj_term p r) ∈ ({⊳} ∪ rstep (wf_rules R) O {⊵})))"
fun
subterm_criterion_proc ::
"'f proj ⇒ ('f, 'v) trs ⇒ ('f, 'v) dpp ⇒ ('f, 'v) dpp ⇒ bool"
where
"subterm_criterion_proc p D (nfs,m,P, Pw, Q, R, Rw) (nfs',m',P', Pw', Q', R', Rw') = (
subterm_criterion_cond p nfs (P ∪ Pw) Q (R ∪ Rw) D ∧
Q' = Q ∧ R' = R ∧ Rw' = Rw ∧ P' = P - D ∧ Pw' = Pw - D ∧ nfs' = nfs ∧ (m' ⟶ m) ∧ (m ∨ NF_terms Q ⊆ NF_trs (R ∪ Rw)))"
fun shift_by :: "(nat ⇒ nat) ⇒ nat ⇒ nat" where
"shift_by f 0 = 0"
| "shift_by f (Suc i) = Suc (f (shift_by f i))"
theorem subset_subterm_criterion_proc:
"subset_proc (subterm_criterion_proc p D)"
unfolding subset_proc_def
proof (intro impI allI)
fix P Pw Q R Rw P' Pw' Q' R' Rw' nfs nfs' m m'
assume proc: "subterm_criterion_proc p D (nfs, m, P, Pw, Q, R, Rw) (nfs', m', P', Pw', Q', R', Rw')"
let ?π = "proj_term p"
let ?R = "R ∪ Rw"
let ?R' = "R' ∪ Rw'"
let ?wfR = "wf_rules ?R"
let ?P = "P ∪ Pw"
let ?P' = "P' ∪ Pw'"
let ?S = "({⊳} ∪ qrstep nfs Q ?R)"
let ?S' = "({⊳} ∪ rstep (wf_rules ?R) O {⊵})"
have wwf: "wwf_qtrs Q ?wfR" by (rule wwf_qtrs_wf_rules)
have "qrstep False Q ?wfR ⊆ qrstep nfs Q ?wfR" using wwf_qtrs_imp_nfs_switch[OF wwf] by blast
also have "… ⊆ qrstep nfs Q ?R" by (rule qrstep_mono, auto simp: wf_rules_def)
finally have wf_to_R: "⋀ st. st ∈ qrstep False Q ?wfR ⟹ st ∈ qrstep nfs Q ?R" by blast
from proc have eqs: "Q' = Q" "R' = R " "Rw' = Rw" "P' = P - D" "Pw' = Pw - D" "nfs' = nfs"
and "?R' ⊆ ?R"
and m_or_inn: "m ∨ NF_terms Q ⊆ NF_trs ?R"
and "m' ⟹ m"
unfolding subterm_criterion_proc.simps by auto
from proc[unfolded subterm_criterion_proc.simps subterm_criterion_cond_def, THEN conjunct1]
have cond: "∀(l, r)∈?P. is_Fun l ∧ is_Fun r ∧ ¬ defined ?R (the (root r))"
and nvar: "∀(l, r)∈?R. is_Fun l"
and weak: "∀(l, r)∈?P - D. ?π l = ?π r"
and strict: "(Q = {} ∧ (∀(l, r)∈D. (?π l, ?π r) ∈ ?S^+))
∨ (∀(l, r)∈D. (?π l, ?π r) ∈ ?S')"
by auto
show "?R' ⊆ ?R ∧ Q' = Q ∧ nfs' = nfs ∧ (m' ⟶ m) ∧ (∀s t σ.
min_ichain (nfs, m, P, Pw, Q, R, Rw) s t σ ⟶
(∃i. ichain (nfs, m', P', Pw', Q', R', Rw') (shift s i) (shift t i) (shift σ i)))"
proof (intro conjI allI impI)
show "?R' ⊆ ?R" by fact
show "Q' = Q" unfolding eqs ..
show "nfs' = nfs" unfolding eqs ..
assume m' thus m by fact
next
fix s t σ assume mchain: "min_ichain (nfs,m,P, Pw, Q, R, Rw) s t σ"
have "∃i. min_ichain (nfs,m,P - D, Pw - D, Q, R, Rw) (shift s i) (shift t i) (shift σ i)"
proof (intro min_ichain_split_P[OF mchain] notI)
assume mchain': "min_ichain (nfs,m,D ∩ ?P, ?P - D, Q, {}, ?R) s t σ"
hence "∀i. ∃j≥i. (s j, t j) ∈ D" by (auto simp: ichain.simps INFM_nat_le)
from choice[OF this] obtain f :: "nat ⇒ nat"
where mono: "∀i. f i ≥ i"
and D_seq: "∀i. (s (f i), t (f i)) ∈ D" by auto
from cond and mchain
have s_no_vars: "⋀ i. is_Fun (s i)"
and t_no_vars: "⋀ i. is_Fun (t i)"
and t_undef: "⋀ i. ¬ defined ?R (the (root (t i)))"
by (auto simp: ichain.simps)
have ts_undef: "⋀ i. ¬ defined ?R (the (root (t i ⋅ σ i)))"
proof -
fix i
from t_no_vars[of i] and t_undef[of i]
show "¬ defined ?R (the (root (t i ⋅ σ i)))" by auto
qed
let ?s = "λi. ?π (s i ⋅ σ i)"
let ?t = "λi. ?π (t i ⋅ σ i)"
{
fix i
from mchain' have "(s i, t i) ∈ D ∩ ?P ∪ (?P - D)" by (auto simp: ichain.simps)
hence "(s i, t i) ∈ D ∪ ?P'" unfolding eqs by blast
hence "(?s i, ?t i) ∈ ?S^*"
proof
assume in_D: "(s i, t i) ∈ D"
from strict
show ?thesis
proof (elim disjE conjE)
assume Q: "Q = {}" and "(∀(l, r)∈D. (?π l, ?π r) ∈ ({⊳} ∪ qrstep nfs Q ?R)^+)"
with in_D have 1: "(?π (s i), ?π (t i)) ∈ ?S^+" by auto
from supt_rstep_trancl_stable[OF 1[unfolded Q qrstep_rstep_conv], of "σ i"]
have "(?s i, ?t i) ∈ ?S^+"
using s_no_vars[of i] and t_no_vars[of i]
by (simp add: Q)
thus ?thesis by simp
next
assume "∀(l, r)∈D. (?π l, ?π r) ∈ {⊳} ∪ rstep ?wfR O {⊵}"
with in_D have "(?π (s i), ?π (t i)) ∈ {⊳} ∪ rstep ?wfR O {⊵}" by blast
thus ?thesis
proof
assume "?π (s i) ⊳ ?π (t i)"
from supt_subst[OF this] have "?π (s i) ⋅ σ i ⊳ ?π (t i) ⋅ σ i" .
thus ?thesis
using s_no_vars[of i]
and t_no_vars[of i]
using proj_term_subst_apply_term_distrib by auto
next
assume step_rhd: "(?π (s i), ?π (t i)) ∈ rstep ?wfR O {⊵}"
from mchain have "s i ⋅ σ i ∈ NF_terms Q" and nfsub: "NF_subst nfs (s i, t i) (σ i) Q" by (auto simp: ichain.simps)
moreover have "s i ⋅ σ i ⊵ ?π (s i) ⋅ σ i"
using supteq_proj_term[of "s i ⋅ σ i"]
unfolding proj_term_subst_apply_term_distrib[OF s_no_vars]
.
ultimately have NF_si: "?π (s i) ⋅ σ i ∈ NF_terms Q" using NF_subterm by blast
from NF_imp_subt_NF[OF this] have NF_terms: "∀u⊲?π (s i) ⋅ σ i. u ∈ NF_terms Q" .
from step_rhd obtain u where step: "(?π (s i), u) ∈ rstep ?wfR" and "u ⊵ ?π (t i)"
by auto
then obtain C l r τ where si: "?π (s i) = C ⟨ l ⋅ τ ⟩" and u: "u = C ⟨ r ⋅ τ ⟩"
and wlr: "(l,r) ∈ ?wfR" by auto
from wlr have vrl: "vars_term r ⊆ vars_term l" unfolding wf_rules_def wf_rule_def by auto
from si have "?π (s i) ⊵ l ⋅ τ" by auto
hence subtl: "?π (s i) ⋅ σ i ⊵ l ⋅ τ ⋅ σ i" by auto
from NF_subterm[OF NF_si this] have NFli: "l ⋅ τ ⋅ σ i ∈ NF_terms Q" .
have "(?π (s i) ⋅ σ i, u ⋅ σ i) ∈ qrstep nfs Q ?R"
unfolding si u subst_apply_term_ctxt_apply_distrib
proof (rule wf_to_R, rule qrstep.ctxt[OF qrstepI[OF _ wlr, of _ _ _ Hole]], unfold ctxt_apply_term.simps, intro allI impI)
show "l ⋅ τ ⋅ σ i = l ⋅ (τ ∘⇩s σ i)" by simp
show "r ⋅ τ ⋅ σ i = r ⋅ (τ ∘⇩s σ i)" by simp
next
fix t
assume "l ⋅ (τ ∘⇩s σ i) ⊳ t"
with NF_imp_subt_NF[OF NFli] show "t ∈ NF_terms Q" by auto
qed simp
moreover from ‹u ⊵ ?π (t i)› have "u ⋅ σ i ⊵ ?π (t i) ⋅ σ i" by auto
ultimately have "(?π (s i) ⋅ σ i, ?π (t i) ⋅ σ i) ∈ qrstep nfs Q ?R O {⊵}"
by auto
thus ?thesis
unfolding proj_term_subst_apply_term_distrib[OF s_no_vars]
unfolding proj_term_subst_apply_term_distrib[OF t_no_vars]
unfolding supteq_supt_set_conv by (rule set_rev_mp) regexp
qed
qed
next
assume "(s i, t i) ∈ ?P'"
with weak have "?π (s i) = ?π (t i)"
unfolding eqs by auto
hence "?π (s i) ⋅ σ i = ?π (t i) ⋅ σ i" by simp
hence "?s i = ?t i"
using s_no_vars[of i] and t_no_vars[of i] by simp
thus ?thesis by simp
qed
} note si_ti = this
have chain: "chain (?S^*) ?s"
proof
fix i
have "(?t i, ?s (Suc i)) ∈ ?S^*"
proof -
from mchain
have "(t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q ?R)^*"
by (simp add: ichain.simps)
from qrsteps_proj_term[OF this ts_undef nvar]
show ?thesis using rtrancl_Un_subset[of "{⊳}" "qrstep nfs Q ?R"]
by auto
qed
with si_ti[of i] show "(?s i, ?s (Suc i)) ∈ ?S^*" by simp
qed
from chain_imp_rtrancl[OF this] and mono
have between: "∀i. (?s i, ?s (f i)) ∈ ?S^*" by simp
let ?s' = "λi. ?π (s (shift_by f (Suc i)) ⋅ σ (shift_by f (Suc i)))"
have "∀i. (?s i, ?s (Suc (f i))) ∈ ?S^+"
proof
fix i
from strict have "(?π (s (f i) ⋅ σ (f i)), ?π (t (f i) ⋅ σ (f i))) ∈ ?S^+"
proof (elim disjE conjE)
assume Q: "Q = {}" and strict: "∀(l, r)∈D. (?π l, ?π r) ∈ ?S^+"
with D_seq have "(?π (s (f i)), ?π (t (f i))) ∈ ?S^+" by blast
from supt_rstep_trancl_stable[OF this[unfolded Q qrstep_rstep_conv]]
show ?thesis
using s_no_vars[of "f i"] t_no_vars[of "f i"] by (simp add: Q)
next
assume "∀(l, r)∈D. (?π l, ?π r) ∈ ?S'"
with D_seq have "(?π (s (f i)), ?π (t (f i))) ∈ ?S'" by auto
thus ?thesis
proof
assume "?π (s (f i)) ⊳ ?π (t (f i))"
from supt_subst[OF this, of "σ (f i)"]
show ?thesis
using s_no_vars[of "f i"]
and t_no_vars[of "f i"]
using proj_term_subst_apply_term_distrib by auto
next
from mchain have "s (f i) ⋅ σ (f i) ∈ NF_terms Q" by (auto simp: ichain.simps)
moreover have "s (f i) ⋅ σ (f i) ⊵ ?π (s (f i)) ⋅ σ (f i)"
using supteq_proj_term[of "s (f i) ⋅ σ (f i)"]
unfolding proj_term_subst_apply_term_distrib[OF s_no_vars]
.
ultimately have NF_si: "?π (s (f i)) ⋅ σ (f i) ∈ NF_terms Q" using NF_subterm by blast
from NF_imp_subt_NF[OF this] have NF_terms: "∀u⊲?π (s (f i)) ⋅ σ (f i). u ∈ NF_terms Q" .
assume "(?π (s (f i)), ?π (t (f i))) ∈ rstep ?wfR O {⊵}"
then obtain u where step: "(?π (s (f i)), u) ∈ rstep ?wfR" and "u ⊵ ?π (t (f i))"
by auto
then obtain C l r τ where si: "?π (s (f i)) = C ⟨ l ⋅ τ ⟩" and u: "u = C ⟨ r ⋅ τ ⟩"
and wlr: "(l,r) ∈ ?wfR" by auto
from si have "?π (s (f i)) ⊵ l ⋅ τ" by auto
hence subtl: "?π (s (f i)) ⋅ σ (f i) ⊵ l ⋅ τ ⋅ σ (f i)" by auto
from NF_subterm[OF NF_si this] have NFli: "l ⋅ τ ⋅ σ (f i) ∈ NF_terms Q" .
have "(?π (s (f i)) ⋅ σ (f i), u ⋅ σ (f i)) ∈ qrstep nfs Q ?R" unfolding si u
proof (rule wf_to_R, rule qrstepI[OF _ wlr], intro allI impI)
show "C ⟨ l ⋅ τ ⟩ ⋅ σ (f i) = (C ⋅⇩c σ (f i)) ⟨ l ⋅ (τ ∘⇩s σ (f i)) ⟩" by simp
show "C ⟨ r ⋅ τ ⟩ ⋅ σ (f i) = (C ⋅⇩c σ (f i)) ⟨ r ⋅ (τ ∘⇩s σ (f i)) ⟩" by simp
next
fix t
assume "l ⋅ (τ ∘⇩s σ (f i)) ⊳ t"
with NF_imp_subt_NF[OF NFli] show "t ∈ NF_terms Q" by auto
qed simp
moreover from ‹u ⊵ ?π (t (f i))› have "u ⋅ σ (f i) ⊵ ?π (t (f i)) ⋅ σ (f i)" by auto
ultimately have step: "(?π (s (f i)) ⋅ σ (f i), ?π (t (f i)) ⋅ σ (f i)) ∈ qrstep nfs Q ?R O {⊵}"
by auto
show ?thesis
by (rule set_mp[OF _ step[unfolded
proj_term_subst_apply_term_distrib[OF s_no_vars]
proj_term_subst_apply_term_distrib[OF t_no_vars]]],
unfold supteq_supt_set_conv, regexp)
qed
qed
with between[THEN spec, of i] have "(?s i, ?π (t (f i) ⋅ σ (f i))) ∈ ?S^+" by simp
moreover have "(?π (t (f i) ⋅ σ (f i)), ?π (s (Suc (f i)) ⋅ σ (Suc (f i)))) ∈ ?S^*"
proof -
from mchain
have "(t (f i) ⋅ σ (f i), s (Suc (f i)) ⋅ σ (Suc (f i))) ∈ (qrstep nfs Q ?R)^*" by (simp add: ichain.simps)
from qrsteps_proj_term[OF this ts_undef nvar, of p]
show ?thesis
using rtrancl_Un_subset[of "{⊳}" "qrstep nfs Q ?R"] by auto
qed
ultimately show "(?s i, ?s (Suc (f i))) ∈ ?S^+" by simp
qed
hence "∀i. (?s' i, ?s' (Suc i)) ∈ ?S^+" by simp
with HOL.refl[of "?s' 0"]
have "∃S. S 0 = ?s' 0 ∧ (∀i. (S i, S (Suc i)) ∈ ?S^+)" by best
hence "¬ SN_on (?S^+) {?s' 0}" unfolding SN_defs by simp
moreover have "SN_on (?S^+) {?s' 0}"
proof -
have "(?t 0, ?s' 0) ∈ (?S^+)^*"
proof -
from mchain have "(t 0 ⋅ σ 0, s (Suc 0) ⋅ σ (Suc 0)) ∈ (qrstep nfs Q ?R)^*" by (simp add: ichain.simps)
from qrsteps_proj_term[OF this ts_undef nvar, of p]
have "(?t 0, ?s (Suc 0)) ∈ ?S^*"
using rtrancl_Un_subset[of "{⊳}" "qrstep nfs Q ?R"] by auto
moreover have "(?s (Suc 0), ?s' 0) ∈ ?S^*"
proof -
have "shift_by f (Suc 0) ≥ Suc 0" by simp
from chain_imp_rtrancl[OF chain this] show ?thesis by simp
qed
ultimately show ?thesis by simp
qed
moreover have "SN_on (?S^+) {?t 0}"
proof -
from m_or_inn have "SN_on (qrstep nfs Q ?R) {?t 0}"
proof
assume m
with mchain m_or_inn have "SN_on (qrstep nfs Q ?R) {t 0 ⋅ σ 0}" by (simp add: minimal_cond_def)
moreover have "(t 0 ⋅ σ 0, ?t 0) ∈ {⊵}" by (simp add: supteq_proj_term)
ultimately show "SN_on (qrstep nfs Q ?R) {?t 0}"
using subterm_preserves_SN_gen[OF ctxt_closed_qrstep, of nfs Q "?R" "t 0 ⋅ σ 0" "?t 0"]
unfolding supt_supteq_conv by force
next
assume "NF_terms Q ⊆ NF_trs ?R"
with mchain have NF: "s 0 ⋅ σ 0 ∈ NF_trs ?R" by (auto simp: ichain.simps)
from supteq_proj_term
have "s 0 ⋅ σ 0 ⊵ ?s 0" .
from NF_subterm[OF NF this] have NF: "?s 0 ∈ NF_trs ?R" .
moreover have "?s 0 ⊵ ?t 0" using si_ti[of 0]
proof (induct)
case (step y z)
from NF_subterm[OF NF step(3)] have NF: "y ∈ NF_trs ?R" .
have "y ∈ NF (qrstep nfs Q ?R)"
by (rule set_mp[OF NF_anti_mono NF], auto)
with step(2) have "y ⊳ z" by auto
with step(3) show ?case
by (metis subterm.dual_order.strict_implies_order subterm.order.strict_trans2)
qed auto
ultimately have NF: "?t 0 ∈ NF_trs ?R" by (rule NF_subterm)
have "?t 0 ∈ NF (qrstep nfs Q ?R)"
by (rule set_mp[OF NF_anti_mono NF], auto)
from NF_imp_SN_on[OF this]
show "SN_on (qrstep nfs Q ?R) {?t 0}" .
qed
from SN_on_trancl[OF SN_on_qrstep_imp_SN_on_supt_union_qrstep[OF this]]
show ?thesis .
qed
ultimately show ?thesis by (rule steps_preserve_SN_on)
qed
ultimately show False ..
qed
thus "∃i. ichain (nfs,m',P',Pw',Q',R',Rw') (shift s i) (shift t i) (shift σ i)"
by (auto simp: eqs ichain.simps)
qed
qed
lemmas subterm_criterion_proc_sound =
subset_proc_to_sound_proc[OF subset_subterm_criterion_proc]
end