[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] TCCS: proved - complete versus incomplete

I have the following TCCS

   1  % Assuming TCC generated (at line 4, column 12) for
   2	% libext@isemirings[boolean, AND, OR, TRUE, FALSE]
   3	% generated from assumption isemirings.zero
   4    % proved - complete
   5  IMP_isemirings_TCC1: OBLIGATION
   6    zero?[boolean](AND)(FALSE);
   7
   8  % Assuming TCC generated (at line 7, column 12) for
   9	% libext@isemirings[boolean, OR, AND, FALSE, TRUE]
  10	% generated from assumption isemirings.zero
  11    % proved - incomplete
  12  IMP_isemirings_TCC4: OBLIGATION
  13    zero?[boolean](OR)(TRUE);

What's the difference between "proved - complete" (line 4) and "proved
- incomplete" (line 11)? Thanks

jerome