[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] nonempty type tcc
I've just changed to version 3.2 and a problem has cropped up.
I have a theory
I import this theory via library, eg,
lib: LIBRARY = "whatever"
The type checker generates the tcc
% Existence TCC generated (at line 97, column 1) for pp: PROC
pp_TCC1: OBLIGATION EXISTS (x: PROC): TRUE;
This isn't proved when I use M-x prove-tccs-theory (ie, using (tcc)
I introduced a theorem identical to pp_TCC1 in theory proc and was able
to prove it straight away using (grind).
How can I prove it as an obligation?