Le 21/05/2019 à 09:48, Raphael Rieu-Helft a écrit :
Dear Evgeny,
With the following change to your program, both invariants are proved
instantly by Alt-Ergo. The reason why the invariants are true is that
the contents of the matrix above the diagonal are unchanged. My change
makes this explic
Dear Evgeny,
With the following change to your program, both invariants are proved
instantly by Alt-Ergo. The reason why the invariants are true is that
the contents of the matrix above the diagonal are unchanged. My change
makes this explicit. In general, as a user I prefer doing this kind of
