WCR ∧ WN ∧ Inc ⇒ SN #
Since this proof requires some proofs from Thesis.ARS and Thesis.Newman, it can't be in BasicProperties along with the rest of the proofs.
theorem
Thesis.not_increasing_of_infinite_common_reduct
{α : Type u_1}
(r : Rel α α)
{f : ℕ → α}
{b : α}
(hseq : Thesis.reduction_seq r⁺ ⊤ f)
(hf : ∀ (n : ℕ), r⁺ (f n) b)
:
If there is an infinite transitive reduction sequence of elements (aₙ) which all reduce to some common element b, then the reduction relation cannot be increasing.
theorem
Thesis.sn_of_wcr_wn_inc
{α : Type u_1}
(r : Rel α α)
(hwcr : Thesis.weakly_confluent r)
(hwn : Thesis.weakly_normalizing r)
(hInc : Thesis.increasing r)
:
Any relation which is WCR, WN, and Inc is SN.