By some peculiarity in the TCC generation by PVS, the theorem USER_LAST_TCC5
in theory gnsl_last seems sometimes to have become a condition very similar
to USER_LAST_TCC3 (and to which the same proof applies) and sometimes this
seems to be subsumed by USER_LAST_TCC3 and replaced by a condition involving
the minimum size of a list. It is the latter for which the proof is given.
pvs-4.2
Folders and files
| Name | Name | Last commit date | ||
|---|---|---|---|---|
parent directory.. | ||||