In this rule, in addition to maintaining the loop invariant, one also proves termination by way of an expression formula_134, called the loop variant, whose value strictly decreases with respect to a well-founded relation formula_135 on some domain set formula_136 during each iteration. Since formula_135 is well-founded, a strictly decreasing chain of members of formula_136 can have only finite length, so formula_134 cannot keep decreasing forever. (For example, the usual order formula_135 is well-founded on positive integers formula_141, but neither on the integers formula_142 nor on positive real numbers formula_143; all these sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)