Well-founded relation

A well-founded relation is a binary relation that has a specific property related to the absence of infinite descending sequences.