def Thesis.Newman.ambiguous {α : Type u_1} (r : Rel α α) (a : α) : Prop

An ambiguous element a has at least two distinct normal forms.

Equations

• Thesis.Newman.ambiguous r a = ∃ (b : α) (c : α), r∗ a b ∧ r∗ a c ∧ Thesis.normal_form r b ∧ Thesis.normal_form r c ∧ b ≠ c

theorem Thesis.Newman.confluent_of_wn_unr ⦃α : Type u_2⦄ ⦃r : Rel α α⦄ (hwn : Thesis.weakly_normalizing r) (hu : Thesis.unique_nf_prop_r r) : Thesis.confluent r

Uniqueness of normal forms + weak normalization implies confluence.

theorem Thesis.Newman.trans_step_of_two_normal_forms {α : Type u_1} {r : Rel α α} {a d₁ d₂ : α} (hd₁ : Thesis.normal_form r d₁) (hd₂ : Thesis.normal_form r d₂) (had₁ : r∗ a d₁) (had₂ : r∗ a d₂) (hne : d₁ ≠ d₂) : r⁺ a d₁ ∧ r⁺ a d₂

If an element has two distinct normal forms, neither one can be the element itself, so the reduction sequences a ->> d₁ and a ->> d₂ must be transitive instead of reflexive-transitive.

theorem Thesis.Newman.exists_ambiguous_reduct_of_ambiguous {α : Type u_1} {r : Rel α α} (hwn : Thesis.weakly_normalizing r) (hwc : Thesis.weakly_confluent r) (a : α) : Thesis.Newman.ambiguous r a → ∃ (b : α), r a b ∧ Thesis.Newman.ambiguous r b

In the context of Newman's lemma, an ambiguous element a always has a one-step reduct which is also ambiguous (leading to an infinite sequence).

theorem Thesis.Newman.not_sn_of_wc_not_un {α : Type u_1} (r : Rel α α) (hwc : Thesis.weakly_confluent r) (hnu : ¬Thesis.unique_nf_prop_r r) : ¬Thesis.strongly_normalizing r

theorem Thesis.Newman.newman {α : Type u_1} (r : Rel α α) (hsn : Thesis.strongly_normalizing r) (hwc : Thesis.weakly_confluent r) : Thesis.confluent r

Newman's lemma: strong normalization + local confluence implies confluence.

instance Thesis.Newman.inv_trans_strict_order_of_sn {α : Type u_1} {r : Rel α α} (hsn : Thesis.strongly_normalizing r) : IsStrictOrder α r.inv⁺

If r is strongly normalizing, the transitive closure of r.inv is a strict order.

Equations

• ⋯ = ⋯

instance Thesis.Newman.wf_inv_trans_of_sn {α : Type u_1} {r : Rel α α} (hsn : Thesis.strongly_normalizing r) : IsWellFounded α r.inv⁺

If r is strongly normalizing, the transitive closure of r.inv is well-founded.

Equations

• ⋯ = ⋯

theorem Thesis.Newman.newman₂ {α : Type u_1} {r : Rel α α} (hsn : Thesis.strongly_normalizing r) (hwc : Thesis.weakly_confluent r) : Thesis.confluent r

Newman's Lemma using well-founded induction w.r.t (r.inv).

theorem Thesis.Newman.newman_step' {α : Type u_1} {r : Rel α α} {x y : α} {ss : List (α × α)} (hwc : Thesis.weakly_confluent r) (hseq : Thesis.ReductionSeq (SymmGen r) x y ss) (hp : hseq.has_peak) : ∃ (ss' : List (α × α)) (hseq' : Thesis.ReductionSeq (SymmGen r) x y ss'), Thesis.MultisetExt r.inv⁺ ↑hseq'.elems ↑hseq.elems

If a landscape contains a peak, there must be a landscape whose elements are smaller than our original landscape according to the multiset order.

theorem Thesis.Newman.newman₃ {α : Type u_1} {r : Rel α α} (hsn : Thesis.strongly_normalizing r) (hwc : Thesis.weakly_confluent r) : Thesis.confluent r

Newman's Lemma, using a terminating peak-elimination procedure.