それでも解けず

５月９日土曜日、晴れ

昨日に続いて証明を試みる。寝たら頭もスッキリしてどうにかなるだろうとおもっていたけれど、さにあらず。無念。
ループ不変条件に指定している

i ≤ n-1 ∧ (∀j < n-1. j ≠ i ⟶ v!j ≤ v!(j+1))

は、とてもきれいだとおもうのだけれど証明できない。

整列済みの右にあった要素を、順次左に送っている。これだけなので、送り終えた部分は元どおり整列済み。それだけの話なんだけれど、これがうまく説明（証明）できない。

どこで引っかかっているのか、もう少しわかりやすく説明してくれるとありがたいんだけれどなあ。なにしろ僕は相手の言葉になおす力が貧弱だし、相手の言葉を受け取る力も弱いのでよくわからない。困った。