Termination (well-foundedness) properties of relations

theorem Relation.normal_iff {α : Type u_1} (r : α → α → Prop) (x : α) : Normal r x ↔ ∀ (y : α), ¬r x y

@[deprecated Relation.normal_iff (since := "2026-09-03")]

theorem Relation.Normal_iff {α : Type u_1} (r : α → α → Prop) (x : α) : Normal r x ↔ ∀ (y : α), ¬r x y

Alias of Relation.normal_iff.

theorem Relation.Normal.reflTransGen_eq {α : Type u_1} {r : α → α → Prop} {x y : α} (h : Normal r x) (xy : ReflTransGen r x y) : x = y

A multi-step from a normal form must be reflexive.

theorem Relation.SN_iff_SN_of_rel {α : Type u_1} {r : α → α → Prop} (x : α) : SN r x ↔ ∀ (y : α), r x y → SN r y

theorem Relation.SN.intro {α : Type u_1} {r : α → α → Prop} {x : α} (h : ∀ (y : α), r x y → SN r y) : SN r x

theorem Relation.SN.of_rel {α : Type u_1} {r : α → α → Prop} {x y : α} (hx : SN r x) (h : r x y) : SN r y

theorem Relation.SN.of_rel_reflTransGen {α : Type u_1} {r : α → α → Prop} {x y : α} (hx : SN r x) (h : ReflTransGen r x y) : SN r y

theorem Relation.SN.transGen {α : Type u_1} {r : α → α → Prop} {x : α} (hx : SN r x) : SN (TransGen r) x

theorem Relation.SN.of_le {α : Type u_1} {r : α → α → Prop} {x : α} {r' : α → α → Prop} (hx : SN r x) (h : r' ≤ r) : SN r' x

@[simp]

theorem Relation.SN.iff_transGen {α : Type u_1} {r : α → α → Prop} (x : α) : SN (TransGen r) x ↔ SN r x

theorem Relation.SN.iff_isEmpty_chain {α : Type u_1} {r : α → α → Prop} {x : α} : SN r x ↔ IsEmpty ↑{f : ℕ → α | f 0 = x ∧ ∀ (n : ℕ), r (f n) (f (n + 1))}

SN r x is equivalent to the more elementary definition, that there is no infinite sequence of reductions starting with x.

theorem Relation.SN.onFun_of_image {α : Type u_1} {β : Sort u_2} {x : α} {r : β → β → Prop} {f : α → β} (hx : SN r (f x)) : SN (Function.onFun r f) x

theorem Relation.SN.of_normal {α : Type u_1} {r : α → α → Prop} {x : α} (hx : Normal r x) : SN r x

theorem Relation.SN.normalizable {α : Type u_1} {r : α → α → Prop} {x : α} (hx : SN r x) : Normalizable r x

theorem Relation.Terminating.apply {α : Type u_1} {r : α → α → Prop} (hr : Terminating r) (x : α) : SN r x

theorem Relation.Terminating.iff_forall_sn {α : Type u_1} {r : α → α → Prop} : Terminating r ↔ ∀ (x : α), SN r x

theorem Relation.Terminating.to_transGen {α : Type u_1} {r : α → α → Prop} (ht : Terminating r) : Terminating (TransGen r)

@[deprecated Relation.Terminating.to_transGen (since := "2026-09-03")]

theorem Relation.Terminating.toTransGen {α : Type u_1} {r : α → α → Prop} (ht : Terminating r) : Terminating (TransGen r)

Alias of Relation.Terminating.to_transGen.

theorem Relation.Terminating.to_acyclic {α : Type u_1} {r : α → α → Prop} (ht : Terminating r) : Acyclic r

A terminating relation is acyclic.

@[deprecated Relation.Terminating.to_acyclic (since := "2026-09-03")]

theorem Relation.Terminating.toAcyclic {α : Type u_1} {r : α → α → Prop} (ht : Terminating r) : Acyclic r

Alias of Relation.Terminating.to_acyclic.

---

A terminating relation is acyclic.

theorem Relation.Terminating.of_transGen {α : Type u_1} {r : α → α → Prop} : Terminating (TransGen r) → Terminating r

@[deprecated Relation.Terminating.of_transGen (since := "2026-09-03")]

theorem Relation.Terminating.ofTransGen {α : Type u_1} {r : α → α → Prop} : Terminating (TransGen r) → Terminating r

Alias of Relation.Terminating.of_transGen.

theorem Relation.Terminating.iff_transGen {α : Type u_1} {r : α → α → Prop} : Terminating (TransGen r) ↔ Terminating r

theorem Relation.Terminating.iff_isEmpty_chain {α : Type u_1} {r : α → α → Prop} : Terminating r ↔ IsEmpty { f : ℕ → α // ∀ (n : ℕ), r (f n) (f (n + 1)) }

theorem Relation.Terminating.of_le {α : Type u_1} {r r' : α → α → Prop} (hr : Terminating r) (h : r' ≤ r) : Terminating r'

theorem Relation.Terminating.subtype_sn {α : Type u_1} (r : α → α → Prop) : Terminating fun (a b : { x : α // SN r x }) => r ↑a ↑b

theorem Relation.Terminating.to_normalizing {α : Type u_1} {r : α → α → Prop} (hr : Terminating r) : Normalizing r

@[deprecated Relation.Terminating.to_normalizing (since := "2026-09-03")]

theorem Relation.Terminating.isNormalizing {α : Type u_1} {r : α → α → Prop} (hr : Terminating r) : Normalizing r

Alias of Relation.Terminating.to_normalizing.