参考while规则以获得完全正确性，WP似乎告诉我，只要找到一个严格减少的循环变量就足以证明终止。我不能接受，要么是因为我遗漏了什么，要么是规则错误。考虑
int i = 1000;
while(true) i--;
其中变量i的值是严格递减的循环变量，但循环肯定不会终止。
当然，规则需要有一个额外的前提条件，比如i<0→B（其中B-是公理模式中的循环条件），使得循环条件最终"捕获"循环变量并退出。
或者我错过了什么？
循环变量必须是一个自然数。自然数不能减少到零以上。使用大词，循环变量是一个相对于有充分基础的关系单调递减的值。你的推理缺少的是有根据的东西。
如维基百科文章所述：
[…]条件B必须暗示t是不是其范围内的最小元素，否则这个规则的前提将是错误的。
在现有情况下，B是true，t为i。true不蕴涵i的极小性，因此不满足该规则的前提。
通常的排序"<"建立在自然数上，但不建立在整数上。为了使关系成立，其域的每个非空子集都必须有一个极小元素。由于可以证明，对于一个有充分基础的关系，不存在无限下降链，因此，具有变体的循环必须终止。
当然，在最小元素的情况下，循环的条件必须为false！
然而，变体不必局限于自然数。无限序数也是有序的。