Theory Rewriting_Properties
section ‹Confluence related rewriting properties›
theory Rewriting_Properties
imports Rewriting
"Abstract-Rewriting.Abstract_Rewriting"
begin
subsection ‹Confluence related ARS properties›
definition "SCR_on r A ≡ (∀a ∈ A. ∀ b c. (a, b) ∈ r ∧ (a, c) ∈ r ⟶
(∃ d. (b, d) ∈ r⇧= ∧ (c, d) ∈ r⇧*))"
abbreviation SCR :: "'a rel ⇒ bool" where "SCR r ≡ SCR_on r UNIV"
definition NFP_on :: "'a rel ⇒ 'a set ⇒ bool" where
"NFP_on r A ⟷ (∀a∈A. ∀b c. (a, b) ∈ r⇧* ∧ (a, c) ∈ r⇧! ⟶ (b, c) ∈ r⇧*)"
abbreviation NFP :: "'a rel ⇒ bool" where "NFP r ≡ NFP_on r UNIV"
definition CE_on :: "'a rel ⇒ 'a rel ⇒ 'a set ⇒ bool" where
"CE_on r s A ⟷ (∀a∈A. ∀b. (a, b) ∈ r⇧↔⇧* ⟷ (a, b) ∈ s⇧↔⇧*)"
abbreviation CE :: "'a rel ⇒ 'a rel ⇒ bool" where "CE r s ≡ CE_on r s UNIV"
definition NE_on :: "'a rel ⇒ 'a rel ⇒ 'a set ⇒ bool" where
"NE_on r s A ⟷ (∀a∈A. ∀b. (a, b) ∈ r⇧! ⟷ (a, b) ∈ s⇧!)"
abbreviation NE :: "'a rel ⇒ 'a rel ⇒ bool" where "NE r s ≡ NE_on r s UNIV"
subsection ‹Signature closure of relation to model multihole context closure›
lemma all_ctxt_closed_sig_rsteps [intro]:
fixes ℛ :: "('f,'v) term rel"
shows "all_ctxt_closed ℱ ((srstep ℱ ℛ)⇧*)" (is "all_ctxt_closed _ (?R⇧*)")
proof (rule trans_ctxt_sig_imp_all_ctxt_closed)
fix C :: "('f,'v) ctxt" and s t :: "('f,'v)term"
assume C: "funas_ctxt C ⊆ ℱ"
and s: "funas_term s ⊆ ℱ"
and t: "funas_term t ⊆ ℱ"
and steps: "(s,t) ∈ ?R⇧*"
from steps
show "(C ⟨ s ⟩, C ⟨ t ⟩) ∈ ?R⇧*"
proof (induct)
case (step t u)
from step(2) have tu: "(t,u) ∈ rstep ℛ" and t: "funas_term t ⊆ ℱ" and u: "funas_term u ⊆ ℱ"
by (auto dest: srstepD)
have "(C ⟨ t ⟩, C ⟨ u ⟩) ∈ ?R" by (rule sig_stepI[OF _ _ rstep_ctxtI[OF tu]], insert C t u, auto)
with step(3) show ?case by auto
qed auto
qed (auto intro: trans_rtrancl)
lemma sigstep_trancl_funas:
"(s, t) ∈ (srstep ℱ 𝒮)⇧* ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ"
"(s, t) ∈ (srstep ℱ 𝒮)⇧* ⟹ s ≠ t ⟹ funas_term t ⊆ ℱ"
by (auto simp: rtrancl_eq_or_trancl dest: srstepsD)
lemma srrstep_to_srestep:
"(s, t) ∈ srrstep ℱ ℛ ⟹ (s, t) ∈ srstep ℱ ℛ"
by (meson in_mono rrstep_rstep_mono sig_step_mono2)
lemma srsteps_with_root_step_srstepsD:
"(s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧+"
by (auto dest: srrstep_to_srestep simp: srsteps_with_root_step_def)
lemma srsteps_with_root_step_sresteps_eqD:
"(s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧*"
by (auto dest: srrstep_to_srestep simp: srsteps_with_root_step_def)
lemma symcl_srstep_conversion:
"(s, t) ∈ srstep ℱ (ℛ⇧↔) ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
by (simp add: conversion_def rstep_converse_dist srstep_symcl_dist)
lemma symcl_srsteps_conversion:
"(s, t) ∈ (srstep ℱ (ℛ⇧↔))⇧* ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
by (simp add: conversion_def rstep_converse_dist srstep_symcl_dist)
lemma NF_srstep_args:
assumes "Fun f ss ∈ NF (srstep ℱ ℛ)" "funas_term (Fun f ss) ⊆ ℱ" "i < length ss"
shows "ss ! i ∈ NF (srstep ℱ ℛ)"
proof (rule ccontr)
assume "ss ! i ∉ NF (srstep ℱ ℛ)"
then obtain t where step: "(ss ! i, t) ∈ rstep ℛ" "funas_term t ⊆ ℱ"
by (auto simp: NF_def sig_step_def)
from assms(3) have [simp]: "Suc (length ss - Suc 0) = length ss" by auto
from rstep_ctxtI[OF step(1), where ?C = "ctxt_at_pos (Fun f ss)[i]"]
have "(Fun f ss, Fun f (ss[i := t])) ∈ srstep ℱ ℛ" using step(2) assms(2, 3)
by (auto simp: sig_step_def upd_conv_take_nth_drop min_def UN_subset_iff
dest: in_set_takeD in_set_dropD simp flip: id_take_nth_drop)
then show False using assms(1)
by (auto simp: NF_def)
qed
lemma all_ctxt_closed_srstep_conversions [simp]:
"all_ctxt_closed ℱ ((srstep ℱ ℛ)⇧↔⇧*)"
by (simp add: all_ctxt_closed_sig_rsteps sig_step_conversion_dist)
lemma NFP_stepD:
"NFP r ⟹ (a, b) ∈ r⇧* ⟹ (a, c) ∈ r⇧* ⟹ c ∈ NF r ⟹ (b, c) ∈ r⇧*"
by (auto simp: NFP_on_def)
lemma NE_symmetric: "NE r s ⟹ NE s r"
unfolding NE_on_def by auto
lemma CE_symmetric: "CE r s ⟹ CE s r"
unfolding CE_on_def by auto
text ‹Reducing the quantification over rewrite sequences for properties @{const CR} ... to
rewrite sequences containing at least one root step›
lemma all_ctxt_closed_sig_reflE:
"all_ctxt_closed ℱ ℛ ⟹ funas_term t ⊆ ℱ ⟹ (t, t) ∈ ℛ"
proof (induct t)
case (Fun f ts)
from Fun(1)[OF nth_mem Fun(2)] Fun(3)
have "i < length ts ⟹ funas_term (ts ! i) ⊆ ℱ" "i < length ts ⟹ (ts ! i, ts ! i) ∈ ℛ" for i
by (auto simp: SUP_le_iff)
then show ?case using all_ctxt_closedD[OF Fun(2)] Fun(3)
by simp
qed (simp add: all_ctxt_closed_def)
lemma all_ctxt_closed_relcomp [intro]:
"(⋀ s t. (s, t) ∈ ℛ ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ) ⟹
(⋀ s t. (s, t) ∈ 𝒮 ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ) ⟹
all_ctxt_closed ℱ ℛ ⟹ all_ctxt_closed ℱ 𝒮 ⟹ all_ctxt_closed ℱ (ℛ O 𝒮)"
proof -
assume funas:"(⋀ s t. (s, t) ∈ ℛ ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ)"
"(⋀ s t. (s, t) ∈ 𝒮 ⟹ s ≠ t ⟹ funas_term s ⊆ ℱ ∧ funas_term t ⊆ ℱ)"
and ctxt_cl: "all_ctxt_closed ℱ ℛ" "all_ctxt_closed ℱ 𝒮"
{fix f ss ts assume ass: "(f, length ss) ∈ ℱ" "length ss = length ts" "⋀ i. i < length ts ⟹ (ss ! i, ts ! i) ∈ (ℛ O 𝒮)"
"⋀ i . i < length ts ⟹ funas_term (ts ! i) ⊆ ℱ" "⋀i. i < length ts ⟹ funas_term (ss ! i) ⊆ ℱ"
from ass(2, 3) obtain us where us: "length us = length ts" "⋀ i. i < length ts ⟹ (ss ! i, us ! i) ∈ ℛ"
"⋀ i. i < length ts ⟹ (us ! i, ts ! i) ∈ 𝒮"
using Ex_list_of_length_P[of "length ts" "λ x i. (ss ! i, x) ∈ ℛ ∧ (x, ts ! i) ∈ 𝒮"]
by auto
from funas have fu: "⋀ i . i < length us ⟹ funas_term (us ! i) ⊆ ℱ" using us ass(4, 5)
by (auto simp: funas_rel_def) (metis in_mono)
have "(Fun f ss, Fun f us) ∈ ℛ" using ass(1, 2, 5) us(1, 2) fu
by (intro all_ctxt_closedD[OF ctxt_cl(1), of f]) auto
moreover have "(Fun f us, Fun f ts) ∈ 𝒮" using ass(1, 2, 4) us(1, 3) fu
by (intro all_ctxt_closedD[OF ctxt_cl(2), of f]) auto
ultimately have "(Fun f ss, Fun f ts) ∈ ℛ O 𝒮" by auto}
moreover
{fix x have "(Var x, Var x) ∈ ℛ" "(Var x, Var x) ∈ 𝒮" using ctxt_cl
by (auto simp: all_ctxt_closed_def)
then have "(Var x, Var x) ∈ ℛ O 𝒮" by auto}
ultimately show ?thesis by (auto simp: all_ctxt_closed_def)
qed
abbreviation "prop_to_rel P ≡ {(s, t)| s t. P s t}"
abbreviation "prop_mctxt_cl ℱ P ≡ all_ctxt_closed ℱ (prop_to_rel P)"
lemma prop_mctxt_cl_Var:
"prop_mctxt_cl ℱ P ⟹ P (Var x) (Var x)"
by (simp add: all_ctxt_closed_def)
lemma prop_mctxt_cl_refl_on:
"prop_mctxt_cl ℱ P ⟹ funas_term t ⊆ ℱ ⟹ P t t"
using all_ctxt_closed_sig_reflE by blast
lemma prop_mctxt_cl_reflcl_on:
"prop_mctxt_cl ℱ P ⟹ funas_term s ⊆ ℱ ⟹ P s s"
using all_ctxt_closed_sig_reflE by blast
lemma reduction_relations_to_root_step:
assumes "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ P s t"
and cl: "prop_mctxt_cl ℱ P"
and well: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
and steps: "(s, t) ∈ (srstep ℱ ℛ)⇧*"
shows "P s t" using steps well
proof (induct s arbitrary: t)
case (Var x)
have "(Var x, t) ∈ (srstep ℱ ℛ)⇧+ ⟹ (Var x, t) ∈ srsteps_with_root_step ℱ ℛ"
using nsrsteps_with_root_step_step_on_args by blast
from assms(1)[OF this] show ?case using Var cl
by (auto simp: rtrancl_eq_or_trancl dest: all_ctxt_closed_sig_reflE)
next
case (Fun f ss) note IH = this show ?case
proof (cases "Fun f ss = t")
case True show ?thesis using IH(2, 4) unfolding True
by (intro prop_mctxt_cl_reflcl_on[OF cl]) auto
next
case False
then have step: "(Fun f ss, t) ∈ (srstep ℱ ℛ)⇧+" using IH(2)
by (auto simp: refl rtrancl_eq_or_trancl)
show ?thesis
proof (cases "(Fun f ss, t) ∈ srsteps_with_root_step ℱ ℛ")
case False
from nsrsteps_with_root_step_step_on_args[OF step this] obtain ts
where *[simp]: "t = Fun f ts" and inv: "length ss = length ts"
"∀ i < length ts. (ss ! i, ts ! i) ∈ (srstep ℱ ℛ)⇧*"
by auto
have funas: "(f, length ts) ∈ ℱ" "∀i<length ts. funas_term (ss ! i) ⊆ ℱ ∧ funas_term (ts ! i) ⊆ ℱ"
using IH(3, 4) step inv(1) by (auto simp: UN_subset_iff)
then have t: "∀ i < length ts. P (ss ! i) (ts ! i)"
using prop_mctxt_cl_reflcl_on[OF cl] IH(1) inv
by (auto simp: rtrancl_eq_or_trancl)
then show ?thesis unfolding * using funas inv(1) all_ctxt_closedD[OF cl]
by auto
qed (auto simp add: assms(1))
qed
qed
abbreviation "comp_rrstep_rel ℱ ℛ 𝒮 ≡ srsteps_with_root_step ℱ ℛ O (srstep ℱ 𝒮)⇧* ∪
(srstep ℱ ℛ)⇧* O srsteps_with_root_step ℱ 𝒮"
abbreviation "comp_rrstep_rel' ℱ ℛ 𝒮 ≡ srsteps_with_root_step ℱ ℛ O (srstep ℱ 𝒮)⇧+ ∪
(srstep ℱ ℛ)⇧+ O srsteps_with_root_step ℱ 𝒮"
lemma reduction_join_relations_to_root_step:
assumes "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮 ⟹ P s t"
and cl: "prop_mctxt_cl ℱ P"
and well: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ"
and steps: "(s, t) ∈ (srstep ℱ ℛ)⇧* O (srstep ℱ 𝒮)⇧*"
shows "P s t" using steps well
proof (induct s arbitrary: t)
case (Var x)
have f: "(Var x, t) ∈ (srstep ℱ ℛ)⇧+ ⟹ (Var x, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮"
using nsrsteps_with_root_step_step_on_args[of "Var x" _ ℱ ℛ] unfolding srsteps_with_root_step_def
by (metis (no_types, lifting) Term.term.simps(4) UnI1 relcomp.relcompI rtrancl_eq_or_trancl)
have s: "(Var x, t) ∈ (srstep ℱ 𝒮)⇧+ ⟹ (Var x, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮"
using nsrsteps_with_root_step_step_on_args[of "Var x" _ ℱ 𝒮] unfolding srsteps_with_root_step_def
by (metis (no_types, lifting) Term.term.simps(4) UnI2 relcomp.simps rtrancl.simps)
have t: "(Var x, u) ∈ (srstep ℱ ℛ)⇧+ ⟹ (u, t) ∈ (srstep ℱ 𝒮)⇧+ ⟹ (Var x, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮" for u
using nsrsteps_with_root_step_step_on_args[of "Var x" u ℱ ℛ] unfolding srsteps_with_root_step_def
by auto (meson relcomp.simps trancl_into_rtrancl)
show ?case using Var f[THEN assms(1)] s[THEN assms(1)] t[THEN assms(1)] cl
by (auto simp: rtrancl_eq_or_trancl prop_mctxt_cl_Var)
next
case (Fun f ss) note IH = this show ?case
proof (cases "Fun f ss = t")
case True show ?thesis using IH(2, 3, 4) cl
by (auto simp: True prop_mctxt_cl_refl_on)
next
case False
obtain u where u: "(Fun f ss, u) ∈ (srstep ℱ ℛ)⇧*" "(u, t) ∈ (srstep ℱ 𝒮)⇧*" using IH(2) by auto
show ?thesis
proof (cases "(Fun f ss, u) ∈ srsteps_with_root_step ℱ ℛ")
case True
then have "(Fun f ss, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮" using u
by (auto simp: srsteps_with_root_step_def)
from assms(1)[OF this] show ?thesis by simp
next
case False note nt_fst = this show ?thesis
proof (cases "(u, t) ∈ srsteps_with_root_step ℱ 𝒮")
case True
then have "(Fun f ss, t) ∈ comp_rrstep_rel ℱ ℛ 𝒮" using u unfolding srsteps_with_root_step_def
by blast
from assms(1)[OF this] show ?thesis by simp
next
case False note no_root = False nt_fst
show ?thesis
proof (cases "Fun f ss = u ∨ u = t")
case True
from assms(1) have f: "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ P s t"
and s: "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ P s t" unfolding srsteps_with_root_step_def
by blast+
have "u = t ⟹ ?thesis" using u cl IH(3, 4)
by (intro reduction_relations_to_root_step[OF f]) auto
moreover have "Fun f ss = u ⟹ ?thesis" using u cl IH(3, 4)
by (intro reduction_relations_to_root_step[OF s]) auto
ultimately show ?thesis using True by auto
next
case False
then have steps: "(Fun f ss, u) ∈ (srstep ℱ ℛ)⇧+" "(u, t) ∈ (srstep ℱ 𝒮)⇧+" using u
by (auto simp: rtrancl_eq_or_trancl)
obtain ts us
where [simp]: "u = Fun f us" and inv_u: "length ss = length us" "∀ i < length ts. (ss ! i, us ! i) ∈ (srstep ℱ ℛ)⇧*"
and [simp]: "t = Fun f ts" and inv_t: "length us = length ts" "∀ i < length ts. (us ! i, ts ! i) ∈ (srstep ℱ 𝒮)⇧*"
using nsrsteps_with_root_step_step_on_args[OF steps(1) no_root(2)]
using nsrsteps_with_root_step_step_on_args[OF steps(2) no_root(1)]
by auto
from inv_u inv_t cl IH(3, 4) have t: "∀ i < length ts. P (ss ! i) (ts ! i)"
by (auto simp: UN_subset_iff intro!: IH(1)[OF nth_mem, of i "ts ! i" for i])
moreover have "(f, length ts) ∈ ℱ" using IH(4) by auto
ultimately show ?thesis using IH(3, 4) inv_u inv_t all_ctxt_closedD[OF cl]
by (auto simp: UN_subset_iff)
qed
qed
qed
qed
qed
definition "commute_redp ℱ ℛ 𝒮 s t ⟷ (s, t) ∈ ((srstep ℱ 𝒮)⇧* O ((srstep ℱ ℛ)¯)⇧*)"
declare subsetI[rule del]
lemma commute_redp_mctxt_cl:
"prop_mctxt_cl ℱ (commute_redp ℱ ℛ 𝒮)"
by (auto simp: commute_redp_def rew_converse_inwards
dest: sigstep_trancl_funas intro!: all_ctxt_closed_relcomp)
declare subsetI[intro!]
lemma commute_rrstep_intro:
assumes "⋀ s t. (s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) 𝒮 ⟹ commute_redp ℱ ℛ 𝒮 s t"
shows "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
proof -
have [simp]: "x ∈ srsteps_with_root_step ℱ 𝒰 ⟹ x ∈ (srstep ℱ 𝒰)⇧* O ℒ⇧*" for x 𝒰 ℒ
by (cases x) (auto dest!: srsteps_with_root_step_sresteps_eqD)
have [simp]: "x ∈ srsteps_with_root_step ℱ 𝒰 ⟹ x ∈ ℒ⇧* O (srstep ℱ 𝒰)⇧*" for x 𝒰 ℒ
by (cases x) (auto dest!: srsteps_with_root_step_sresteps_eqD)
have red: "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) 𝒮 ⟹ commute_redp ℱ ℛ 𝒮 s t" using assms
unfolding commute_redp_def srstep_converse_dist
by (auto simp: rtrancl_eq_or_trancl) blast+
have comI: "(⋀ s t. (s, t) ∈ ((srstep ℱ (ℛ¯))⇧*) O (srstep ℱ 𝒮)⇧* ⟹ commute_redp ℱ ℛ 𝒮 s t) ⟹
commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
by (auto simp: commute_redp_def commute_def subsetD rew_converse_inwards)
show ?thesis
using reduction_join_relations_to_root_step[OF red commute_redp_mctxt_cl, of "ℛ¯" 𝒮]
by (intro comI, auto) (metis (no_types, lifting) commute_redp_def relcompI rew_converse_inwards sigstep_trancl_funas srstep_converse_dist)
qed
lemma commute_to_rrstep:
assumes "commute (srstep ℱ ℛ) (srstep ℱ 𝒮)"
shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) 𝒮 ⟹ commute_redp ℱ ℛ 𝒮 s t" using assms
unfolding commute_def commute_redp_def srstep_converse_dist
by (auto simp: srstep_converse_dist dest: srsteps_with_root_step_sresteps_eqD)
lemma CR_Aux:
assumes "⋀ s t. (s, t) ∈ (srstep ℱ (ℛ¯))⇧* O srsteps_with_root_step ℱ ℛ ⟹ commute_redp ℱ ℛ ℛ s t"
shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ commute_redp ℱ ℛ ℛ s t"
proof -
have sym: "commute_redp ℱ ℛ ℛ s t ⟹ commute_redp ℱ ℛ ℛ t s" for s t
by (auto simp: commute_redp_def) (metis converseI relcomp.relcompI rtrancl_converse rtrancl_converseD)
{fix s t assume "(s, t) ∈ (srstep ℱ ℛ)⇧* O srsteps_with_root_step ℱ (ℛ¯)"
then have "commute_redp ℱ ℛ ℛ s t" unfolding commute_redp_def
by (auto simp: srsteps_with_root_step_def rew_converse_inwards dest!: srrstep_to_srestep)}
note * = this
{fix s t assume ass: "(s, t) ∈ srsteps_with_root_step ℱ (ℛ¯) O (srstep ℱ ℛ)⇧*"
have [dest!]: "(u, t) ∈ (srstep ℱ ℛ)⇧* ⟹ (t, u) ∈ (sig_step ℱ ((rstep ℛ)¯))⇧*" for u
by (metis rew_converse_outwards rtrancl_converseI srstep_converse_dist)
from ass have "(t, s) ∈ (srstep ℱ (ℛ¯))⇧* O srsteps_with_root_step ℱ ℛ"
unfolding srsteps_with_root_step_def rstep_converse_dist
by (metis (mono_tags, lifting) O_assoc converse.simps converse_converse converse_inward(1) converse_relcomp rew_converse_outwards(1, 2) sig_step_converse_rstep)
from assms[OF this] have "commute_redp ℱ ℛ ℛ s t" using sym by blast}
then show "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ commute_redp ℱ ℛ ℛ s t" unfolding srsteps_with_root_step_def
by (metis UnE assms srsteps_with_root_step_def)
qed
lemma CR_rrstep_intro:
assumes "⋀ s t. (s, t) ∈ (srstep ℱ (ℛ¯))⇧+ O srsteps_with_root_step ℱ ℛ ⟹ commute_redp ℱ ℛ ℛ s t"
shows "CR (srstep ℱ ℛ)"
proof -
{fix s u assume "(s, u) ∈ (srstep ℱ (ℛ¯))⇧* O srsteps_with_root_step ℱ ℛ"
then obtain t where a: "(s, t) ∈ (srstep ℱ (ℛ¯))⇧*" "(t, u) ∈ srsteps_with_root_step ℱ ℛ" by blast
have "commute_redp ℱ ℛ ℛ s u"
proof (cases "s = t")
case [simp]: True
from srsteps_with_root_step_srstepsD[OF a(2)] show ?thesis
by (auto simp: commute_redp_def)
next
case False
then have "(s, t) ∈ (srstep ℱ (ℛ¯))⇧+" using a(1) unfolding rtrancl_eq_or_trancl
by simp
then show ?thesis using assms a(2) by blast
qed}
from commute_rrstep_intro[OF CR_Aux[OF this]]
show ?thesis unfolding CR_iff_self_commute
by (metis Un_iff reflcl_trancl relcomp_distrib relcomp_distrib2)
qed
lemma CR_to_rrstep:
assumes "CR (srstep ℱ ℛ)"
shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ commute_redp ℱ ℛ ℛ s t" using assms
using commute_to_rrstep[OF assms[unfolded CR_iff_self_commute]]
by simp
definition NFP_redp where
"NFP_redp ℱ ℛ s t ⟷ t ∈ NF (srstep ℱ ℛ) ⟶ (s, t) ∈ (srstep ℱ ℛ)⇧*"
lemma prop_mctxt_cl_NFP_redp:
"prop_mctxt_cl ℱ (NFP_redp ℱ ℛ)"
proof -
{fix f ts ss assume sig: "(f, length ss) ∈ ℱ" "length ts = length ss"
and steps: "∀ i < length ss. ss ! i ∈ NF (srstep ℱ ℛ) ⟶ (ts ! i, ss ! i) ∈ (srstep ℱ ℛ)⇧*"
and funas: "∀ i < length ss. funas_term (ts ! i) ⊆ ℱ ∧ funas_term (ss ! i) ⊆ ℱ"
and NF: "Fun f ss ∈ NF (srstep ℱ ℛ)"
from steps have steps: "i < length ss ⟹ (ts ! i, ss ! i) ∈ (srstep ℱ ℛ)⇧*" for i
using sig funas NF_srstep_args[OF NF]
by (auto simp: UN_subset_iff) (metis in_set_idx)
then have "(Fun f ts, Fun f ss) ∈ (srstep ℱ ℛ)⇧*" using sig
by (metis all_ctxt_closed_def all_ctxt_closed_sig_rsteps funas le_sup_iff)}
then show ?thesis
by (auto simp: NFP_redp_def all_ctxt_closed_def)
qed
lemma NFP_rrstep_intro:
assumes "⋀ s t. (s, t) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ⟹ NFP_redp ℱ ℛ s t"
shows "NFP (srstep ℱ ℛ)"
proof -
from assms have red: "⋀ t u. (t, u) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ NFP_redp ℱ ℛ t u"
apply (auto simp: NFP_redp_def rtrancl_eq_or_trancl)
apply (metis NF_no_trancl_step converseD srstep_converse_dist srsteps_with_root_step_srstepsD trancl_converse)
apply blast
apply (meson NF_no_trancl_step srsteps_with_root_step_srstepsD)
by blast
have "⋀ s t. (s, t) ∈ (sig_step ℱ ((rstep ℛ)¯))⇧* O (srstep ℱ ℛ)⇧* ⟹ NFP_redp ℱ ℛ s t"
using reduction_join_relations_to_root_step[OF red prop_mctxt_cl_NFP_redp, of "ℛ¯" ℛ]
by (auto simp: NFP_redp_def) (metis (no_types, lifting) relcomp.relcompI rstep_converse_dist rtranclD srstepsD)
then show ?thesis unfolding NFP_on_def NFP_redp_def
by (auto simp: normalizability_def) (metis meetI meet_def rstep_converse_dist srstep_converse_dist)
qed
lemma NFP_lift_to_conversion:
assumes "NFP r" "(s, t) ∈ (r⇧↔)⇧*" and "t ∈ NF r"
shows "(s, t) ∈ r⇧*" using assms(2, 3)
proof (induct rule: converse_rtrancl_induct)
case (step s u)
then have "(u, t) ∈ r⇧!" by auto
then show ?case using assms(1) step(1) unfolding NFP_on_def
by auto
qed simp
lemma NFP_to_rrstep:
assumes "NFP (srstep ℱ ℛ)"
shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ NFP_redp ℱ ℛ s t" using assms
using NFP_lift_to_conversion[OF assms] unfolding NFP_redp_def srsteps_with_root_step_def
by auto (metis (no_types, lifting) r_into_rtrancl rstep_converse_dist rtrancl_trans srrstep_to_srestep srstep_symcl_dist)
definition "UN_redp ℱ ℛ s t ⟷ s ∈ NF (srstep ℱ ℛ) ∧ t ∈ NF (srstep ℱ ℛ) ⟶ s = t"
lemma prop_mctxt_cl_UN_redp:
"prop_mctxt_cl ℱ (UN_redp ℱ ℛ)"
proof -
{fix f ts ss assume sig: "(f, length ss) ∈ ℱ" "length ts = length ss"
and steps: "∀ i < length ss. ts ! i ∈ NF (srstep ℱ ℛ) ∧ ss ! i ∈ NF (srstep ℱ ℛ) ⟶ ts ! i = ss ! i"
and funas: "∀ i < length ss. funas_term (ts ! i) ⊆ ℱ ∧ funas_term (ss ! i) ⊆ ℱ"
and NF: "Fun f ts ∈ NF (srstep ℱ ℛ)" "Fun f ss ∈ NF (srstep ℱ ℛ)"
from steps have steps: "i < length ss ⟹ ts ! i = ss ! i" for i
using sig funas NF_srstep_args[OF NF(1)] NF_srstep_args[OF NF(2)]
by (auto simp: UN_subset_iff) (metis in_set_idx)
then have "Fun f ts = Fun f ss" using sig(2)
by (simp add: nth_equalityI)}
then show ?thesis
by (auto simp: UN_redp_def all_ctxt_closed_def)
qed
lemma UNC_rrstep_intro:
assumes"⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ UN_redp ℱ ℛ s t"
shows "UNC (srstep ℱ ℛ)"
proof -
have "⋀ s t. (s, t) ∈ (srstep ℱ (ℛ⇧↔))⇧* ⟹ UN_redp ℱ ℛ s t"
using reduction_relations_to_root_step[OF assms(1) prop_mctxt_cl_UN_redp, of "ℛ⇧↔"]
by (auto simp: UN_redp_def) (meson rtranclD srstepsD)
then show ?thesis unfolding UNC_def UN_redp_def
by (auto simp: sig_step_conversion_dist)
qed
lemma UNC_to_rrstep:
assumes "UNC (srstep ℱ ℛ)"
shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ UN_redp ℱ ℛ s t"
using assms unfolding UNC_def UN_redp_def srsteps_with_root_step_def
by (auto dest!: srrstep_to_srestep symcl_srstep_conversion symcl_srsteps_conversion)
(metis (no_types, opaque_lifting) conversion_def rtrancl_trans)
lemma UNF_rrstep_intro:
assumes "⋀ t u. (t, u) ∈ comp_rrstep_rel' ℱ (ℛ¯) ℛ ⟹ UN_redp ℱ ℛ t u"
shows "UNF (srstep ℱ ℛ)"
proof -
from assms have red: "⋀ t u. (t, u) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ UN_redp ℱ ℛ t u"
apply (auto simp: UN_redp_def rtrancl_eq_or_trancl)
apply (metis NF_no_trancl_step converseD srstep_converse_dist srsteps_with_root_step_srstepsD trancl_converse)
apply blast
apply (meson NF_no_trancl_step srsteps_with_root_step_srstepsD)
by blast
have "⋀ s t. (s, t) ∈ (sig_step ℱ ((rstep ℛ)¯))⇧* O (srstep ℱ ℛ)⇧* ⟹ UN_redp ℱ ℛ s t"
using reduction_join_relations_to_root_step[OF red prop_mctxt_cl_UN_redp, of "ℛ¯" ℛ]
by (auto simp: UN_redp_def) (metis (no_types, lifting) relcomp.relcompI rstep_converse_dist rtranclD srstepsD)
then show ?thesis unfolding UNF_on_def UN_redp_def
by (auto simp: normalizability_def) (metis meetI meet_def rstep_converse_dist srstep_converse_dist)
qed
lemma UNF_to_rrstep:
assumes "UNF (srstep ℱ ℛ)"
shows "⋀ s t. (s, t) ∈ comp_rrstep_rel ℱ (ℛ¯) ℛ ⟹ UN_redp ℱ ℛ s t"
using assms unfolding UNF_on_def UN_redp_def normalizability_def srsteps_with_root_step_def
by (auto simp flip: srstep_converse_dist dest!: srrstep_to_srestep)
(metis (no_types, lifting) rstep_converse_dist rtrancl.rtrancl_into_rtrancl rtrancl_converseD rtrancl_idemp srstep_converse_dist)+
lemma CE_rrstep_intro:
assumes "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ (s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*"
and "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (𝒮⇧↔) ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
shows "CE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
using reduction_relations_to_root_step[OF assms(1), where ?s1 = "λ s t. s" and ?t1 = "λ s t. t", of ℱ "ℛ⇧↔"]
using reduction_relations_to_root_step[OF assms(2), where ?s1 = "λ s t. s" and ?t1 = "λ s t. t", of ℱ "𝒮⇧↔"]
by (auto simp: CE_on_def)
(metis converseI conversion_converse rtrancl_eq_or_trancl sig_step_conversion_dist sigstep_trancl_funas(1, 2))+
lemma CE_to_rrstep:
assumes "CE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (ℛ⇧↔) ⟹ (s, t) ∈ (srstep ℱ 𝒮)⇧↔⇧*"
"⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ (𝒮⇧↔) ⟹ (s, t) ∈ (srstep ℱ ℛ)⇧↔⇧*"
using assms unfolding CE_on_def srsteps_with_root_step_def
by (auto simp flip: srstep_converse_dist dest!: srrstep_to_srestep symcl_srsteps_conversion symcl_srstep_conversion)
(metis converse_rtrancl_into_rtrancl conversion_rtrancl)+
definition NE_redp where
"NE_redp ℱ ℛ 𝒮 s t ⟷ t ∈ NF (srstep ℱ ℛ) ⟶ t ∈ NF (srstep ℱ ℛ) ⟶ (s, t) ∈ (srstep ℱ 𝒮)⇧*"
lemma prop_mctxt_cl_NE_redp:
"prop_mctxt_cl ℱ (NE_redp ℱ ℛ 𝒮)"
proof -
{fix f ts ss assume sig: "(f, length ss) ∈ ℱ" "length ts = length ss"
and steps: "∀ i < length ss. ss ! i ∈ NF (srstep ℱ ℛ) ⟶ (ts ! i, ss ! i) ∈ (srstep ℱ 𝒮)⇧*"
and funas: "∀ i < length ss. funas_term (ts ! i) ⊆ ℱ ∧ funas_term (ss ! i) ⊆ ℱ"
and NF: "Fun f ss ∈ NF (srstep ℱ ℛ)"
from steps have steps: "i < length ss ⟹ (ts ! i, ss ! i) ∈ (srstep ℱ 𝒮)⇧*" for i
using sig funas NF_srstep_args[OF NF]
by (auto simp: UN_subset_iff) (metis in_set_idx)
then have "(Fun f ts, Fun f ss) ∈ (srstep ℱ 𝒮)⇧*" using sig
by (metis all_ctxt_closed_def all_ctxt_closed_sig_rsteps funas le_sup_iff)}
then show ?thesis
by (auto simp: all_ctxt_closed_def NE_redp_def)
qed
lemma NE_rrstep_intro:
assumes "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ NE_redp ℱ ℛ 𝒮 s t"
and "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ NE_redp ℱ 𝒮 ℛ s t"
and "NF (srstep ℱ ℛ) = NF (srstep ℱ 𝒮)"
shows "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
using assms(3)
using reduction_relations_to_root_step[OF assms(1) prop_mctxt_cl_NE_redp, of ℛ]
using reduction_relations_to_root_step[OF assms(2) prop_mctxt_cl_NE_redp, of 𝒮]
by (auto simp: NE_on_def NE_redp_def normalizability_def)
(metis rtrancl.rtrancl_refl sigstep_trancl_funas)+
lemma NE_to_rrstep:
assumes "NE (srstep ℱ ℛ) (srstep ℱ 𝒮)"
shows "⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ ℛ ⟹ NE_redp ℱ ℛ 𝒮 s t"
"⋀ s t. (s, t) ∈ srsteps_with_root_step ℱ 𝒮 ⟹ NE_redp ℱ 𝒮 ℛ s t"
using assms unfolding NE_on_def NE_redp_def srsteps_with_root_step_def
by (auto simp: normalizability_def simp flip: srstep_converse_dist
dest!: srrstep_to_srestep) (meson converse_rtrancl_into_rtrancl rtrancl_trans)+
lemma NE_NF_eq:
"NE ℛ 𝒮 ⟹ NF ℛ = NF 𝒮"
by (auto simp: NE_on_def NF_def normalizability_def)
abbreviation "SCRp ℱ ℛ t u ≡ ∃v. (t, v) ∈ (srstep ℱ ℛ)⇧= ∧ (u, v) ∈ (srstep ℱ ℛ)⇧*"
lemma SCR_rrstep_intro:
assumes "⋀ s t u. (s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s, u) ∈ srstep ℱ ℛ ⟹ SCRp ℱ ℛ t u"
and "⋀ s t u. (s, t) ∈ srstep ℱ ℛ ⟹ (s, u) ∈ sig_step ℱ (rrstep ℛ) ⟹ SCRp ℱ ℛ t u"
shows "SCR (srstep ℱ ℛ)"
proof -
{fix s t u assume step: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
from step(1) obtain p l r σ where st: "p ∈ poss s" "(l, r) ∈ ℛ" "s |_ p = l ⋅ σ" "t = s[p ← r ⋅ σ]"
using rstep_to_pos_replace[of s t ℛ] unfolding sig_step_def by blast
from step(2) obtain q l2 r2 σ2 where su: "q ∈ poss s" "(l2, r2) ∈ ℛ" "s |_ q = l2 ⋅ σ2" "u = s[q ← r2 ⋅ σ2]"
using rstep_to_pos_replace[of s u ℛ] unfolding sig_step_def by blast
from step st su have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
by (auto dest: srstepD)
have funas2 :"funas_term (r2 ⋅ σ2) ⊆ ℱ" using funas_term_replace_at_lower[OF su(1)]
using funas(3) unfolding su(4) by blast
consider (a) "p ≤⇩p q" | (b) "q ≤⇩p p" | (c) "p ⊥ q"
using position_par_def by blast
then have "SCRp ℱ ℛ t u"
proof cases
case a
from a have up: "p ∈ poss u" using st(1) su(1) unfolding st(4) su(4)
by (metis pos_replace_at_pres position_less_eq_def poss_append_poss)
let ?C = "ctxt_at_pos s p" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) st(1)
by (metis ctxt_at_pos_subt_at_id funas_ctxt_apply le_sup_iff)
from funas have funas: "funas_term (s |_ p) ⊆ ℱ" "funas_term (t |_ p) ⊆ ℱ" "funas_term (u |_ p) ⊆ ℱ"
using a st(1) pos_replace_at_pres[OF st(1)] up unfolding st(4) su(4)
by (intro funas_term_subterm_atI, blast+)+
have "(s |_ p, t |_ p) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (metis poss_of_termE poss_of_term_replace_term_at rrstep.intros sig_stepI st(4))
moreover have "(s |_ p, u |_ p) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (smt (verit, best) a ctxt_at_pos_subt_at_pos ctxt_of_pos_term_apply_replace_at_ident position_less_eq_def
poss_append_poss replace_subterm_at_itself replace_term_at_subt_at_id rstepI sig_stepI su(4))
ultimately obtain v where "(t |_ p, v) ∈ (srstep ℱ ℛ)⇧=" "(u |_ p, v) ∈ (srstep ℱ ℛ)⇧*"
using assms(1) by blast
from this(1) srsteps_eq_ctxt_closed[OF fc this(2)]
show ?thesis using a st(1) su(1) srsteps_eq_ctxt_closed[OF fc] unfolding st(4) su(4)
apply (intro exI[of _ "?C⟨v⟩"])
apply (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
apply (metis ctxt_of_pos_term_apply_replace_at_ident fc srstep_ctxt_closed)
done
next
case b
then have up: "q ∈ poss t" using st(1) su(1) unfolding st(4) su(4)
by (metis pos_replace_at_pres position_less_eq_def poss_append_poss)
let ?C = "ctxt_at_pos s q" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) su(1)
by (metis Un_subset_iff ctxt_at_pos_subt_at_id funas_ctxt_apply)
from funas have funas: "funas_term (s |_ q) ⊆ ℱ" "funas_term (t |_ q) ⊆ ℱ" "funas_term (u |_ q) ⊆ ℱ"
using su(1) pos_replace_at_pres[OF su(1)] up unfolding st(4) su(4)
by (intro funas_term_subterm_atI, blast+)+
have "(s |_ q, t |_ q) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (smt (verit, del_insts) b ctxt_at_pos_subt_at_pos ctxt_of_pos_term_apply_replace_at_ident
position_less_eq_def poss_append_poss replace_subterm_at_itself replace_term_at_subt_at_id rstepI sig_stepI st(4))
moreover have "(s |_ q, u |_ q) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (metis poss_of_termE poss_of_term_replace_term_at rrstep.intros sig_stepI su(4))
ultimately obtain v where "(t |_ q, v) ∈ (srstep ℱ ℛ)⇧=" "(u |_ q, v) ∈ (srstep ℱ ℛ)⇧*"
using assms(2) by blast
from this(1) srsteps_eq_ctxt_closed[OF fc this(2)]
show ?thesis using b st(1) su(1) srsteps_eq_ctxt_closed[OF fc] unfolding st(4) su(4)
apply (intro exI[of _ "?C⟨v⟩"])
apply (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
apply (smt (verit, best) ctxt_of_pos_term_apply_replace_at_ident fc less_eq_subt_at_replace replace_term_at_above replace_term_at_subt_at_id srstep_ctxt_closed)
done
next
case c
define v where "v = t[q ← r2 ⋅ σ2]"
have funasv: "funas_term v ⊆ ℱ" using funas su(1) unfolding v_def su(4)
using funas_term_replace_at_upper funas2 by blast
from c have *: "v = u[p ← r ⋅ σ]" unfolding v_def st(4) su(4) using st(1) su(1)
using parallel_replace_term_commute by blast
from c have "(t, v) ∈ rstep ℛ" unfolding st(4) v_def
using su(1 - 3) par_pos_replace_pres[OF su(1)]
by (metis par_pos_replace_term_at pos_replace_to_rstep position_par_def)
moreover from c have "(u, v) ∈ rstep ℛ" unfolding su(4) *
using st(1 - 3) par_pos_replace_pres[OF st(1)]
by (intro pos_replace_to_rstep[of _ _ l]) (auto simp: par_pos_replace_term_at)
ultimately show ?thesis using funas(2-) funasv
by auto
qed}
then show ?thesis unfolding SCR_on_def
by blast
qed
lemma SCE_to_rrstep:
assumes "SCR (srstep ℱ ℛ)"
shows "⋀ s t u. (s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s, u) ∈ srstep ℱ ℛ ⟹ SCRp ℱ ℛ t u"
"⋀ s t u. (s, t) ∈ srstep ℱ ℛ ⟹ (s, u) ∈ sig_step ℱ (rrstep ℛ) ⟹ SCRp ℱ ℛ t u"
using assms unfolding SCR_on_def srsteps_with_root_step_def
by (auto simp flip: srstep_converse_dist dest!: srrstep_to_srestep symcl_srsteps_conversion symcl_srstep_conversion)
lemma WCR_rrstep_intro:
assumes "⋀ s t u. (s, t) ∈ sig_step ℱ (rrstep ℛ) ⟹ (s, u) ∈ srstep ℱ ℛ ⟹ (t, u) ∈ (srstep ℱ ℛ)⇧↓"
shows "WCR (srstep ℱ ℛ)"
proof -
{fix s t u assume step: "(s, t) ∈ srstep ℱ ℛ" "(s, u) ∈ srstep ℱ ℛ"
from step(1) obtain p l r σ where st: "p ∈ poss s" "(l, r) ∈ ℛ" "s |_ p = l ⋅ σ" "t = s[p ← r ⋅ σ]"
using rstep_to_pos_replace[of s t ℛ] unfolding sig_step_def by blast
from step(2) obtain q l2 r2 σ2 where su: "q ∈ poss s" "(l2, r2) ∈ ℛ" "s |_ q = l2 ⋅ σ2" "u = s[q ← r2 ⋅ σ2]"
using rstep_to_pos_replace[of s u ℛ] unfolding sig_step_def by blast
from step st su have funas: "funas_term s ⊆ ℱ" "funas_term t ⊆ ℱ" "funas_term u ⊆ ℱ"
by (auto dest: srstepD)
have funas2 :"funas_term (r2 ⋅ σ2) ⊆ ℱ" using funas_term_replace_at_lower[OF su(1)]
using funas(3) unfolding su(4) by blast
consider (a) "p ≤⇩p q" | (b) "q ≤⇩p p" | (c) "p ⊥ q"
using position_par_def by blast
then have "(t, u) ∈ (srstep ℱ ℛ)⇧↓"
proof cases
case a
then have up: "p ∈ poss u" using st(1) su(1) unfolding st(4) su(4)
by (metis pos_replace_at_pres position_less_eq_def poss_append_poss)
let ?C = "ctxt_at_pos s p" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) st(1)
by (metis Un_subset_iff ctxt_at_pos_subt_at_id funas_ctxt_apply)
from funas have funas: "funas_term (s |_ p) ⊆ ℱ" "funas_term (t |_ p) ⊆ ℱ" "funas_term (u |_ p) ⊆ ℱ"
using a st(1) pos_replace_at_pres[OF st(1)] up unfolding st(4) su(4)
by (intro funas_term_subterm_atI, blast+)+
have "(s |_ p, t |_ p) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (metis poss_of_termE poss_of_term_replace_term_at rrstep.intros sig_stepI st(4))
moreover have "(s |_ p, u |_ p) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (smt (verit, ccfv_threshold) a greater_eq_subt_at_replace less_eq_subt_at_replace pos_diff_append_itself
pos_replace_to_rstep position_less_eq_def poss_append_poss replace_term_at_subt_at_id sig_stepI su(4))
ultimately have "(t |_ p, u |_ p) ∈ (srstep ℱ ℛ)⇧↓"
using assms(1) by blast
from sig_steps_join_ctxt_closed[OF fc this(1)]
show ?thesis using a st(1) su(1) srstep_ctxt_closed[OF fc] unfolding st(4) su(4)
by (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
next
case b
then have up: "q ∈ poss t" using st(1) su(1) unfolding st(4) su(4)
by (metis pos_les_eq_append_diff pos_replace_at_pres poss_append_poss)
let ?C = "ctxt_at_pos s q" have fc: "funas_ctxt ?C ⊆ ℱ" using funas(1) su(1)
by (metis Un_subset_iff ctxt_at_pos_subt_at_id funas_ctxt_apply)
from funas have funas: "funas_term (s |_ q) ⊆ ℱ" "funas_term (t |_ q) ⊆ ℱ" "funas_term (u |_ q) ⊆ ℱ"
using su(1) pos_replace_at_pres[OF su(1)] up unfolding st(4) su(4)
by (intro funas_term_subterm_atI, blast+)+
have "(s |_ q, t |_ q) ∈ srstep ℱ ℛ" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (smt (verit, ccfv_SIG) b greater_eq_subt_at_replace less_eq_subt_at_replace pos_diff_append_itself
pos_replace_to_rstep position_less_eq_def poss_append_poss replace_term_at_subt_at_id sig_stepI st(4))
moreover have "(s |_ q, u |_ q) ∈ sig_step ℱ (rrstep ℛ)" unfolding st(4) su(4) using st(1 - 3) su(1 - 3) funas
by (metis poss_of_termE poss_of_term_replace_term_at rrstep.intros sig_stepI su(4))
ultimately have "(t |_ q, u |_ q) ∈ (srstep ℱ ℛ)⇧↓"
using assms(1) by blast
from sig_steps_join_ctxt_closed[OF fc this(1)]
show ?thesis using b st(1) su(1) srstep_ctxt_closed[OF fc] unfolding st(4) su(4)
by (auto simp: ctxt_of_pos_term_apply_replace_at_ident less_eq_subt_at_replace)
next
case c
define v where "v = t[q ← r2 ⋅ σ2]"
have funasv: "funas_term v ⊆ ℱ" using funas su(1) unfolding v_def su(4)
using funas_term_replace_at_upper funas2 by blast
from c have *: "v = u[p ← r ⋅ σ]" unfolding v_def st(4) su(4) using st(1) su(1)
using parallel_replace_term_commute by blast
from c have "(t, v) ∈ rstep ℛ" unfolding st(4) v_def
using su(1 - 3) par_pos_replace_pres[OF su(1)]
by (metis par_pos_replace_term_at pos_replace_to_rstep position_par_def)
moreover from c have "(u, v) ∈ rstep ℛ" unfolding su(4) *
using st(1 - 3) par_pos_replace_pres[OF st(1)]
by (metis par_pos_replace_term_at pos_replace_to_rstep)
ultimately show ?thesis using funas(2-) funasv
by auto
qed}
then show ?thesis unfolding WCR_on_def
by blast
qed
end