loops - 減少する反復によるループ不変条件

Question

from (temp := num)
until (temp = index)
loop
{
   data[temp] := data[temp – 1]
   temp := temp – 1
}

したがって、これは (temp) から when (temp=index) までのループです。ループの不変式が何であるかはわかりません。これまで反復回数を減らす作業をしたことがないからです。

(∃i : temp...index) • (data[i] := data[i-1]) のようなものを考えていますが、基本ケースが機能しないため正しくありません。