# existskwantor problem

```Hello,

I'm working on a problem which acts on subsets of some specific sets.
Here is an simplified example of my problem:

First of all I have defined my own types and some specific constants of
that type:

State: Type+

StateS1: State
StateS2: State
StateS3: State
StateRoot: State

After that, I need a set that contains all defined stateconstants.

StateSet: type+ = finite_set[State]

I also need a record which contains two elements:
- the first member: is the set of all stateconstants
- the second member: defines a special state among those stateconstants

StateRecord : type+ = [# States : StateSet,
Root : State #]

Define a specific record with the above constants

Root   := StateRoot #)

Now I define another set of states, which contains or must contain a
subset of the set of all stateconstants, but the Root always has to be a
member of this set.

AState : type+ = finite_set[State]

Because my problem has to search for such sets and it is not very good to
define such sets (like C1) by myself because there can be to many (and it
must be used with model-checking) And now the problem
arises:

The first theorem ("existstheorem") returns a QED. So there exists a
correctly formed subset which is C1. If I reject the second argument
(c=C1) I expect also a QED because we know there exists a correctly formed
subset. (C1 or another subset that contains the RootState). However this
QED is not generated.

existstheorem: theorem exists(c:AState | subset?(c, States(sm))):
member(Root(sm), c) and c=C1
existstheorem2: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c)

What am I missing? How can I force PVS to return a QED.
I also included the dumpfile.

Thx for the help,

Sara

```
```
%% PVS Version 3.0
%% 6.2 [Linux (x86)] (Dec 19, 2002 3:09)
\$\$\$problem.pvs
problem : theory
begin

% Define some specific types and elements of that type
State: Type+

StateS1: State
StateS2: State
StateS3: State
StateRoot: State

% Define a set that contains State-elements
StateSet: type+ = finite_set[State]

% Define the following record
StateRecord : type+ = [# States : StateSet,
Root : State #]

% Define a specific record
Root   := StateRoot #)

% Define another sets of states
AState : type+ = finite_set[State]

% Now I want to check the following theorem
% Does there exists a set, subset of States, which contains the RootState?
%  (it must be automatically be found...)
% The first theorem returns QED ... doest such a set can be found

% The second theorem doesn`t return that. However we know that such a set exists, so
% I expect also a QED. What am I missing here?
existstheorem: theorem exists(c:AState | subset?(c, States(sm))):
member(Root(sm), c) and c=C1
existstheorem2: theorem exists(c:AState | subset?(c, States(sm))): member(Root(sm), c)

end problem

\$\$\$problem.prf
(problem
(existstheorem 0
(existstheorem-1 nil 3223270809 3223270893 ("" (grind) nil nil)
unchecked
((C1 const-decl "AState" problem nil)
(member const-decl "bool" sets nil)
(sm const-decl "StateRecord" problem nil)
(emptyset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil))
7765 170 t shostak))
(existstheorem2 0
(existstheorem2-1 nil 3223270991 3223270995 ("" (grind) nil nil)
proved
((sm const-decl "StateRecord" problem nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)