theory Size_Change_Termination_Processors
imports
Size_Change_Termination
Generic_Usable_Rules
Subterm_Criterion
"Check-NT.Dependency_Graph"
begin
fun get_arg :: "('f, 'v) term ⇒ nat ⇒ ('f, 'v) term" where
"get_arg t 0 = t"
| "get_arg t (Suc n) = args t ! n"
lemma (in redtriple) sct_semantics: "sct_semantics S (NS ∪ NST)"
by (rule sct_semantics.intro, rule SN, rule both.compat)
lemma generic_sct_redtriple:
fixes P :: "('f,'v)trs" and R :: "('f,'v)rules" and Gs :: "('a :: compare_order, nat) scg list"
and info :: "('f,'v)rule ⇒ 'a"
defines sts: "sts ≡ {(s,get_arg t j) | s t j . ∃ st ns. Scg (info (s,t)) (info (s,t)) st ns ∈ set Gs ∧ j ∈ snd ` set st ∪ snd ` set ns}"
assumes tuple: "∀ (s,t) ∈ P. is_Fun s ∧ is_Fun t ∧ ¬ defined (set R) (the (root t))"
and var_R: "⋀ l r. (l,r) ∈ set R ⟹ is_Fun l"
and checker: "usable_rules_checker checker"
and U: "set U ⊆ NS"
and redtriple: "ce_af_redtriple S NS NST π"
and Ucheck: "checker nfs m (wwf_qtrs Q (set R)) π Q R U_opt sts = Some U"
and graphs: "∀ (s,t) ∈ P. ∃ stri non_stri. (
Scg (info (s,t)) (info (s,t)) ( stri) ( non_stri) ∈ set Gs ∧
(∀ (i,j) ∈ set stri. i ≤ length (args s) ∧ j ≤ length (args t) ∧ (get_arg s i, get_arg t j) ∈ S) ∧
(∀ (i,j) ∈ set non_stri. i ≤ length (args s) ∧ j ≤ length (args t) ∧ (get_arg s i, get_arg t j) ∈ NST))"
and edg: "⋀ st uv. (st,uv) ∈ DG nfs m P Q (set R) ⟹ edg (info st) (info uv)"
and check: "check_SCT (λ i_st i_uv. edg i_st i_uv) Gs" (is "check_SCT ?conn Gs")
and P: "P = Ps ∪ Pw" and R: "set R = set Rs ∪ set Rw"
shows "finite_dpp (nfs,m,Ps,Pw,Q,set Rs,set Rw)"
proof -
interpret ce_af_redtriple S NS NST π by fact
let ?rd = "λ x. x"
show ?thesis
proof (rule finite_dpp_mono)
show "finite_dpp (nfs,m,P,{},Q,set R,{})" unfolding finite_dpp_def
proof (clarify)
fix s t σ
assume chain: "min_ichain (nfs,m,P, {}, Q, set R, {}) s t σ"
have ce: "ce_af_redpair S NS π" ..
let ?R = "qrstep nfs Q (set R)"
let ?Rs = "?R^*"
note checker[unfolded usable_rules_checker_def, rule_format, OF Ucheck ce U]
then obtain I where I: "⋀ s t u σ τ. (s,t) ∈ sts ⟹ s ⋅ σ ∈ NF_terms Q ⟹ NF_subst nfs (s,t) σ Q ⟹ (t ⋅ σ, u ⋅ τ) ∈ ?Rs ⟹ (m ⟹ SN_on ?R {t ⋅ σ}) ⟹ (t ⋅ I σ, u ⋅ I τ) ∈ NS^*" by blast
let ?entry = "λ k. (info (s k,t k))"
let ?Is = "λ i. I (σ i)"
let ?pairs = "λ k. (?entry k, (λ j. get_arg (s k) j ⋅ ?Is k))"
let ?R = "{(?pairs k, ?pairs (Suc k)) | k. True}"
let ?S = "(NS ∪ NST ∪ S)⇧* O S O (NS ∪ NST ∪ S)⇧*"
let ?NS = "(NS ∪ NST ∪ S)⇧*"
{
fix k
let ?sk = "λ i. get_arg (s k) i ⋅ σ k"
let ?tk = "λ i. get_arg (t k) i ⋅ σ k"
let ?sk1 = "λ i. args (s (Suc k)) ! i ⋅ σ (Suc k)"
let ?Isk = "λ i. get_arg (s k) i ⋅ ?Is k"
let ?Itk = "λ i. get_arg (t k) i ⋅ ?Is k"
let ?Isk1 = "λ i. get_arg (s (Suc k)) i ⋅ ?Is (Suc k)"
from chain have inP': "(s (Suc k), t (Suc k)) ∈ P" by (auto simp: ichain.simps)
from chain have inP: "(s k, t k) ∈ P" by (auto simp: ichain.simps)
with tuple have validDP: "is_Fun (t k) ∧ ¬ defined (set R) (the (root (t k)))" by auto
from chain inP tuple have validDP1: "is_Fun (s (Suc k))" by (auto simp: ichain.simps)
from chain have steps: "(t k ⋅ σ k, s (Suc k) ⋅ σ (Suc k)) ∈ ?Rs" by (auto simp: ichain.simps)
from chain have NF: "(s k ⋅ σ k) ∈ NF_terms Q" by (auto simp: ichain.simps)
from chain have NFs: "(s (Suc k) ⋅ σ (Suc k)) ∈ NF_terms Q" by (auto simp: ichain.simps)
from chain have nfs: "NF_subst nfs (s k, t k) (σ k) Q" by (auto simp: ichain.simps)
from chain have nfs': "NF_subst nfs (s (Suc k), t (Suc k)) (σ (Suc k)) Q" by (auto simp: ichain.simps)
from chain have tSN: "m ⟹ SN_on (qrstep nfs Q (set R)) {t k ⋅ σ k}" by (simp add: minimal_cond_def)
have argSteps: "⋀ j. j ≤ length (args (t k)) ⟹ (s k, get_arg (t k) j) ∈ sts ⟹ (?Itk j, ?Isk1 j) ∈ NS^*"
proof -
fix j1
assume j1: "j1 ≤ length (args (t k))" and mem: "(s k, get_arg (t k) j1) ∈ sts"
note I = I[OF mem NF]
show "(?Itk j1, ?Isk1 j1) ∈ NS^*"
proof (cases j1)
case 0
show ?thesis
by (rule I, unfold 0, insert steps tSN nfs, auto)
next
case (Suc j)
with j1 have j: "j < length (args (t k))" by auto
note I = I[unfolded Suc get_arg.simps]
let ?tj = "args (t k) ! j"
let ?sj = "args (s (Suc k)) ! j"
from validDP obtain f ts where tk: "t k = Fun f ts ∧ ¬ defined (set R) (f,length ts)" by (cases "t k", auto)
from validDP1 obtain g ss where sk1: "s (Suc k) = Fun g ss" by (cases "s (Suc k)", auto)
let ?tss = "(map (λ t. t ⋅ σ k) ts)"
from tk have f: "¬ defined (set R) (f, length ?tss)" by simp
let ?sss = "(map (λ s. s ⋅ σ (Suc k)) ss)"
from tSN have SN: "m ⟹ SN_on (qrstep nfs Q (set R)) {Fun f ?tss}" using tk by auto
from tk j have "?tj ∈ set ts" by auto
hence "vars_term ?tj ⊆ vars_term (t k)" using tk by auto
with nfs have nfs: "NF_subst nfs (s k, ?tj) (σ k) Q" unfolding NF_subst_def vars_rule_def by auto
note I = I[OF this]
from tk j have mem: "?tj ⋅ σ k ∈ set ?tss" by auto
from steps have "(Fun f ts ⋅ σ k, Fun g ss ⋅ σ (Suc k)) ∈ ?Rs" using tk sk1 by auto
hence steps2: "(Fun f ?tss, Fun g ?sss) ∈ ?Rs" by auto
have "∃ us. length us = length ?tss ∧ Fun g ?sss = Fun f us ∧ (∀ i < length ?tss. (?tss ! i, us ! i) ∈ ?Rs)"
by (rule nondef_root_imp_arg_qrsteps[OF steps2], insert var_R f, force+)
from this obtain us where nearly: "length us = length ?tss ∧ Fun g ?sss = Fun f us ∧ (∀ i < length ?tss. (?tss ! i, us ! i) ∈ ?Rs)" ..
from nearly j tk sk1 have "(?tj ⋅ σ k, ?sj ⋅ σ (Suc k)) ∈ ?Rs" (is ?part1) by auto
have SN2: "m ⟹ SN_on (qrstep nfs Q (set R)) {?tj ⋅ σ k}"
by (rule SN_imp_SN_arg_gen[OF ctxt_closed_qrstep SN mem])
note I = I[OF ‹?part1› SN2]
thus ?thesis unfolding Suc by simp
qed
qed
from steps have rsteps: "(t k ⋅ σ k, s (Suc k) ⋅ σ (Suc k)) ∈ (rstep (set R))^*"
using rtrancl_mono[OF qrstep_subset_rstep] by auto
have "((s k, t k), (s (Suc k), t (Suc k))) ∈ DG nfs m P Q (set R)"
by (rule DG_I[OF inP inP' steps NF NFs nfs nfs' tSN])
from edg[OF this]
have conn: "?conn (?entry k) (?entry (Suc k))" by auto
from inP obtain stri non_stri where graph: "Scg (?entry k) (?entry k) (?rd stri) (?rd non_stri) ∈ set Gs ∧
(∀ (i,j) ∈ set stri. i ≤ length (args (s k)) ∧ j ≤ length (args (t k)) ∧ (get_arg (s k) i, get_arg (t k) j) ∈ S) ∧
(∀ (i,j) ∈ set non_stri. i ≤ length (args (s k)) ∧ j ≤ length (args (t k)) ∧ (get_arg (s k) i, get_arg (t k) j) ∈ NST)" using graphs by force
let ?g = "Scg (?entry k) (?entry k) (?rd stri) (?rd non_stri)"
from graph have gGs: "?g ∈ set Gs" ..
let ?check = "λ g. ((?entry k, ?Isk), (?entry (Suc k)), ?Isk1)
∈ sct_semantics.steps S (NS ∪ NST) ?conn g"
have "?check ?g"
proof (simp add: sct_semantics.steps.simps sct_semantics conn[simplified], intro conjI)
{
fix i j
assume ij: "(i,j) ∈ set non_stri"
with graph have i: "i ≤ length (args (s k))" and j: "j ≤ length (args (t k))"
and NS: "(get_arg (s k) i, get_arg (t k) j) ∈ NST" by auto
have "(s k, get_arg (t k) j) ∈ sts" unfolding sts using graph[THEN conjunct1] ij by force
from argSteps[OF j this]
have astepsNS: "(?Itk j, ?Isk1 j) ∈ NS^*" .
from NS subst_NST have non_strict: "(?Isk i, ?Itk j) ∈ NST" unfolding subst.closed_def using subst.closure.intros by blast
have NS: "(?Isk i, ?Isk1 j) ∈ NST O NS^*" using astepsNS non_strict by blast
have "(?Isk i, ?Isk1 j) ∈ ?NS" by (rule set_mp[OF _ NS], regexp)
}
thus "∀ij∈set non_stri. (λ(i, j). (?Isk i, ?Isk1 j) ∈ ?NS) ij" by blast
next
{
fix i j
assume ij: "(i,j) ∈ set stri"
with graph have i: "i ≤ length (args (s k))" and j: "j ≤ length (args (t k))"
and S: "(get_arg (s k) i, get_arg (t k) j) ∈ S" by auto
have "(s k, get_arg (t k) j) ∈ sts" unfolding sts using graph[THEN conjunct1] ij by force
from argSteps[OF j this]
have astepsNS: "(?Itk j, ?Isk1 j) ∈ NS^*" .
from S subst_S have strict: "(?Isk i, ?Itk j) ∈ S" unfolding subst.closed_def using subst.closure.intros by blast
have S: "(?Isk i, ?Isk1 j) ∈ S O NS^*" using strict astepsNS by blast
have "(?Isk i, ?Isk1 j) ∈ ?S" by (rule set_mp[OF _ S], regexp)
}
thus "∀ij∈set stri.(λ(i, j). (?Isk i, ?Isk1 j) ∈ ?S) ij" by auto
qed
with gGs have "∃ g ∈ set Gs. ?check g" by auto
}
hence main: "?R ⊆ (⋃G ∈ set Gs. sct_semantics.steps S (NS ∪ NST) ?conn G)" by auto
have "SN ?R"
by (rule sct_semantics.SCT_correctness2[where S = S and NS = "NS ∪ NST"], rule sct_semantics, rule main, rule check)
obtain f where "f = ?pairs" by auto
hence id: "?R = {(f k, f (Suc k)) | k. True}" by auto
have "¬ SN ?R" unfolding SN_defs by (simp only: id, blast)
with ‹SN ?R› show False by auto
qed
qed (auto simp: R P)
qed
lemma sct_with_subterm:
assumes chain: "min_ichain (nfs,m,P, {}, Q, R, {}) s t σ"
and tuple: "∀(s, t)∈P. is_Fun s ∧ is_Fun t ∧ ¬ defined R (the (root t))"
and graphs: "∀(s, t)∈P. ∃stri nstri. (
Scg (info (s, t)) (info (s, t)) (remdups_sort stri) (remdups_sort nstri) ∈ set Gs
∧ (∀(i, j)∈set stri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ (get_arg s i, get_arg t j) ∈ supt)
∧ (∀(i, j)∈set nstri.
i ≤ length (args s) ∧ j ≤ length (args t) ∧ (get_arg s i, get_arg t j) ∈ supteq))"
and no_left_vars: "∀(l, r)∈R. is_Fun l"
and m_or_inn: "m ∨ NF_terms Q ⊆ NF_trs R"
and edg: "⋀ st uv. (st,uv) ∈ DG nfs m P Q R ⟹ edg (info st) (info uv)"
and check: "check_SCT (λ i_st i_uv. edg i_st i_uv) Gs" (is "check_SCT ?conn Gs")
shows False
proof -
let ?entry = "λk. info (s (Suc k), t (Suc k))"
let ?s = "λi. s (Suc i)"
let ?t = "λi. t (Suc i)"
let ?σ = "λi. σ (Suc i)"
let ?qrstep = "qrstep nfs Q R"
let ?supt = "restrict_SN (({⊳} ∪ ?qrstep)^+) ?qrstep"
let ?supteq = "restrict_SN (?qrstep^* ) ?qrstep"
let ?pairs = "λk. (?entry k, (λj. get_arg (?s k) j ⋅ ?σ k))"
let ?Rs = "?qrstep^*"
let ?R = "{(?pairs k, ?pairs(Suc k)) | k. True}"
let ?S = "(?supteq ∪ ?supt)^* O ?supt O (?supteq ∪ ?supt)^*"
let ?NS = "(?supteq ∪ ?supt)^*"
have sct_semantics: "sct_semantics ?supt ?supteq"
proof
show "SN ?supt"
proof -
have "∀t. SN_on ?supt {t}"
proof (rule ccontr)
assume "¬(∀t. SN_on ?supt {t})"
then obtain t where "¬ SN_on ?supt {t}" by auto
then obtain S where "S 0 = t" and "∀i. (S i, S (Suc i)) ∈ ?supt"
unfolding SN_defs by auto
hence "∀i. SN_on ?qrstep {S i}" unfolding restrict_SN_def by simp
hence "SN_on ?qrstep {S 0}" by simp
hence "SN_on ({⊳} ∪ ?qrstep) {t}" unfolding ‹S 0 = t›
by (rule SN_on_qrstep_imp_SN_on_supt_union_qrstep)
hence "SN_on (({⊳} ∪ ?qrstep)^+) {t}" by (rule SN_on_trancl)
moreover have "?supt ⊆ ({⊳} ∪ ?qrstep)^+" by (rule restrict_SN_subset)
ultimately have "SN_on ?supt {t}" by (rule SN_on_subset1)
with ‹¬ SN_on ?supt {t}› show False by simp
qed
thus ?thesis unfolding SN_defs by simp
qed
next
show "?supteq O ?supt ⊆ ?supt"
proof (rule subrelI)
fix s t assume "(s, t) ∈ ?supteq O ?supt"
then obtain u where fst: "(s, u) ∈ ?supteq" and snd: "(u, t) ∈ ?supt" by auto
have "(s, u) ∈ ?Rs" and "SN_on ?qrstep {s}" using fst unfolding restrict_SN_def by auto
moreover have "(u, t) ∈ ({⊳} ∪ ?qrstep)^+" and "SN_on ?qrstep {u}" using snd
unfolding restrict_SN_def by auto
ultimately show "(s, t) ∈ ?supt"
proof (induct)
case base thus ?case unfolding restrict_SN_def by simp
next
case (step v w)
from ‹(v, w) ∈ ?qrstep› have "(v, w) ∈ ?qrstep^+" by simp
with trancl_union_right[where r="?qrstep" and s="{⊳}"]
have "(v, w) ∈ ({⊳} ∪ ?qrstep)^+" by blast
with ‹(w, t) ∈ ({⊳} ∪ ?qrstep)^+› have "(v, t) ∈ ({⊳} ∪ ?qrstep)^+" by simp
moreover have "SN_on ?qrstep {v}"
by (rule steps_preserve_SN_on[OF ‹(s, v) ∈ ?Rs› ‹SN_on ?qrstep {s}›])
ultimately show ?case using step by simp
qed
qed
qed
from chain
have inR: "∀k. (t k ⋅ σ k, s (Suc k) ⋅ σ (Suc k)) ∈ ?qrstep^*" by (auto simp: ichain.simps)
{
fix k
{
assume "NF_terms Q ⊆ NF_trs R"
with chain have NF: "?s k ⋅ ?σ k ∈ NF_trs R" by (auto simp: ichain.simps)
} note NF = this
from m_or_inn have min_s: "SN_on ?qrstep {?s k ⋅ ?σ k}"
proof
assume NFQ: "NF_terms Q ⊆ NF_trs R"
show ?thesis
by (rule NF_imp_SN_on[OF set_mp[OF NF_anti_mono NF[OF NFQ]]], auto)
next
assume m
with chain have min_t: "SN_on ?qrstep {t k ⋅ σ k}" by (auto simp: minimal_cond_def)
from inR have step: "(t k ⋅ σ k, ?s k ⋅ ?σ k) ∈ ?qrstep^*" by auto
from steps_preserve_SN_on[OF step min_t] show "SN_on ?qrstep {?s k ⋅ ?σ k}" .
qed
note min_s NF
} note min_s = this
{
fix k
let ?sk = "λi. get_arg (?s k) i ⋅ ?σ k"
let ?tk = "λi. get_arg (?t k) i ⋅ ?σ k"
let ?sk1 = "λi. get_arg (?s (Suc k)) i ⋅ ?σ (Suc k)"
from chain have inP: "(?s k, ?t k) ∈ P" by (auto simp: ichain.simps)
from chain have inP': "(?s (Suc k), ?t (Suc k)) ∈ P" by (auto simp: ichain.simps)
from chain have inR: "(?t k ⋅ ?σ k, ?s (Suc k) ⋅ ?σ (Suc k)) ∈ ?qrstep^*"
by (auto simp: ichain.simps)
have tk_supt: "∀i≤length (args (?t k)). i > 0 ⟶ ?t k ⋅ ?σ k ⊳ ?tk i"
proof (intro impI allI)
fix i assume i: "i ≤ length (args (?t k))"
and i2: "i > 0"
thus "?t k ⋅ ?σ k ⊳ ?tk i"
proof (cases "?t k")
case (Var x) with tuple and inP show ?thesis by auto
next
case (Fun f ss)
from i2 obtain j where j2: "i = Suc j" by (cases i, auto)
with i have j: "j < length (args (?t k))" by auto
from j have "?t k ⊳ args (?t k) ! j" unfolding Fun
using supt.arg[of "args (Fun f ss) ! j" "ss" f] by auto
thus ?thesis using j2 supt_subst[to_set] by auto
qed
qed
have sk_supt: "∀i≤length (args (?s k)). i > 0 ⟶ ?s k ⋅ ?σ k ⊳ ?sk i"
proof (intro impI allI)
fix i assume i: "i ≤ length (args (?s k))"
and i2: "i > 0" thus "?s k ⋅ ?σ k ⊳ ?sk i"
proof (cases "?s k")
case (Var x) with tuple and inP show ?thesis by auto
next
case (Fun f ss)
from i2 obtain j where j2: "i = Suc j" by (cases i, auto)
with i have j: "j < length (args (?s k))" by auto
from j have "?s k ⊳ args (?s k) ! j" unfolding Fun
using supt.arg[of "args (Fun f ss) ! j" "ss" f] by auto
thus ?thesis using j2 supt_subst[to_set] by auto
qed
qed
have SN_sk: "SN_on ?qrstep {?s k ⋅ ?σ k}" using min_s by simp
have SN_ski: "∀i≤length (args (?s k)). SN_on ?qrstep {?sk i}"
proof
fix i
show "i ≤ length(args(?s k)) ⟶ SN_on ?qrstep {?sk i}"
using subterm_preserves_SN_gen[OF ctxt_closed_qrstep SN_sk] sk_supt SN_sk
by (cases i) auto
qed
note chain = chain[unfolded min_ichain.simps ichain.simps minimal_cond_def]
from inP tuple
have validDP: "is_Fun (?t k) ∧ ¬ defined R (the (root (?t k)))"
by auto
from chain inP tuple have validDP1: "is_Fun (?s (Suc k))" by auto
from chain have steps: "(?t k ⋅ ?σ k, ?s(Suc k) ⋅ ?σ(Suc k)) ∈ ?Rs" by auto
{
fix j1
assume j1: "j1 ≤ length (args (?t k))"
and sntk: "SN_on ?qrstep {?tk j1 }"
have "(?tk j1, ?sk1 j1) ∈ ?NS"
proof (cases j1)
case 0
with steps show ?thesis unfolding restrict_SN_def using sntk by auto
next
case (Suc j)
let ?tj = "args (?t k) ! j"
let ?sj = "args (?s (Suc k)) ! j"
from j1 Suc have j: "j < length (args (?t k))" by simp
from validDP obtain f ts
where tk: "?t k = Fun f ts ∧ ¬ defined R (f, length ts)" by (cases "?t k") auto
from validDP1 obtain g ss
where sk1: "?s (Suc k) = Fun g ss" by (cases "?s (Suc k)") auto
let ?tss = "map (λt. t ⋅ ?σ k) ts"
let ?sss = "map (λs. s ⋅ ?σ (Suc k)) ss"
from tk have f: "¬ defined R (f, length ?tss)" by simp
from steps have "(Fun f ts ⋅ ?σ k, Fun g ss ⋅ ?σ (Suc k)) ∈ ?Rs" using tk sk1 by auto
hence steps2: "(Fun f ?tss, Fun g ?sss) ∈ ?Rs" by auto
from this no_left_vars f
have "∃us. length us = length ?tss
∧ Fun g ?sss = Fun f us
∧ (∀i<length ?tss. (?tss ! i, us ! i) ∈ ?Rs)"
by (rule nondef_root_imp_arg_qrsteps)
from this obtain us
where nearly: "length us = length ?tss
∧ Fun g ?sss = Fun f us
∧ (∀i<length ?tss. (?tss ! i, us ! i) ∈ ?Rs)" ..
from sntk have SN_tkj: "SN_on ?qrstep {?tj ⋅ ?σ k}" using j1 Suc by auto
from nearly j tk sk1 have "(?tj ⋅ ?σ k, ?sj ⋅ ?σ (Suc k)) ∈ ?Rs" by auto
with SN_tkj have "(?tj ⋅ ?σ k, ?sj ⋅ ?σ (Suc k)) ∈ restrict_SN ?Rs ?qrstep"
unfolding restrict_SN_def by simp
thus ?thesis using Suc unfolding restrict_SN_def by auto
qed
} note stepsNS = this
have DG: "((?s k, ?t k), (?s (Suc k), ?t (Suc k))) ∈ DG nfs m P Q R"
by (rule DG_I[OF inP inP' steps], insert chain, auto)
from edg[OF this]
have conn: "?conn (?entry k) (?entry (Suc k))" by auto
let ?rd = remdups_sort
from inP obtain stri nstri
where graph: "Scg (?entry k) (?entry k) (?rd stri) (?rd nstri) ∈ set Gs
∧ (∀(i, j)∈set stri.
i ≤ length (args (?s k)) ∧ j ≤ length (args (?t k))
∧ get_arg (?s k) i ⊳ get_arg (?t k) j)
∧ (∀(i, j)∈set nstri.
i ≤ length (args (?s k)) ∧ j ≤ length (args (?t k))
∧ get_arg (?s k) i ⊵ get_arg (?t k) j)" using graphs by force
let ?g = "Scg (?entry k) (?entry k) (?rd stri) (?rd nstri)"
from graph have gGs: "?g ∈ set Gs" ..
let ?check = "λg. ((?entry k, ?sk), (?entry (Suc k), ?sk1))
∈ sct_semantics.steps ?supt ?supteq ?conn g"
{
fix i j
assume i: "i ≤ length(args(?s k))" and j: "j ≤ length(args(?t k))"
and NS: "get_arg(?s k) i ⊵ get_arg (?t k) j"
from m_or_inn have "SN_on ?qrstep {?tk j}"
proof
assume "NF_terms Q ⊆ NF_trs R"
from min_s(2)[OF this] have NF: "?s k ⋅ ?σ k ∈ NF_trs R" .
from tuple inP have "is_Fun (?s k)" by auto
with i have "?s k ⊵ get_arg(?s k) i" by (cases i, auto)
with NS have "?s k ⊵ get_arg (?t k) j"
by (metis subterm.dual_order.trans)
hence subt: "?s k ⋅ ?σ k ⊵ get_arg (?t k) j ⋅ ?σ k" by auto
show ?thesis
by (rule NF_imp_SN_on[OF set_mp[OF NF_anti_mono NF_subterm[OF NF subt]]], auto)
next
assume m
with chain have SN: "SN_on ?qrstep {?t k ⋅ ?σ k}" by auto
have subt: "?t k ⋅ ?σ k ⊵ get_arg (?t k) j ⋅ ?σ k " using j validDP by (cases j, cases "?t k", auto)
show ?thesis by (rule ctxt_closed_SN_on_subt [OF ctxt_closed_qrstep SN subt])
qed
} note SN = this
have "?check ?g"
proof (simp add: sct_semantics.steps.simps sct_semantics conn[simplified], rule conjI)
{
fix i j
assume ij: "(i, j) ∈ set nstri"
with graph have i: "i ≤ length(args(?s k))" and j: "j ≤ length(args(?t k))"
and NS: "get_arg(?s k) i ⊵ get_arg (?t k) j" by auto
have astepsNS: "(?tk j, ?sk1 j) ∈ ?NS"
by (rule stepsNS[OF j SN[OF i j NS]])
from SN_ski and i have snski: "SN_on ?qrstep {?sk i}" by simp
from NS subst_closed_supteq have "?sk i ⊵ ?tk j"
unfolding subst.closed_def using subst.closure.intros by blast
hence non_strict: "(?sk i, ?tk j) ∈ ?NS" using snski
unfolding restrict_SN_def supteq_supt_conv by force
from rtrancl_trans[OF non_strict astepsNS] have "(?sk i, ?sk1 j) ∈ ?NS" by auto
}
thus "∀ij∈set nstri.(λ(i, j). (?sk i, ?sk1 j) ∈ ?NS) ij" by auto
next
{
fix i j
assume "(i, j) ∈ set stri"
with graph have i: "i ≤ length (args(?s k))" and j: "j ≤ length(args(?t k))"
and S: "get_arg(?s k) i ⊳ get_arg(?t k) j" by auto
have astepsNS: "(?tk j, ?sk1 j) ∈ ?NS"
by (rule stepsNS[OF j SN[OF i j]], insert S, auto)
from SN_ski and i have snski: "SN_on ?qrstep {?sk i}" by simp
from S subst_closed_supt have "?sk i ⊳ ?tk j"
unfolding subst.closed_def using subst.closure.intros by blast
hence strict: "(?sk i, ?tk j) ∈ ?supt" using snski
unfolding restrict_SN_def by force
have "(?sk i, ?sk1 j) ∈ ?S" using strict astepsNS by auto
}
thus "∀ij∈set stri.(λ(i, j). (?sk i, ?sk1 j) ∈ ?S) ij" by auto
qed
with gGs have "∃g∈set Gs. ?check g" by blast
}
hence main: "?R ⊆ (⋃G∈set Gs. sct_semantics.steps ?supt ?supteq ?conn G)" by auto
have "SN ?R"
by (rule sct_semantics.SCT_correctness2[where S = ?supt and NS = ?supteq],rule sct_semantics,rule main,rule check)
obtain f where "f = ?pairs" by auto
hence id: "?R = {(f k, f (Suc k)) | k. True}" by auto
have "¬ SN ?R" unfolding SN_defs by (simp only: id, blast)
with ‹SN ?R› show False by auto
qed
end