# A property I cannot prove in PVS

```

Tamarah Arons writes:
>
> I have a question on how to prove a certain property in PVS:
>
> There is a set B of 2*N elements labeled 1 ... 2*N.
>
> 1. Array A of N elements contains N distinct elements from B.
>
> 2. List L can contain up to N elements. The elements in L are
>    distinct and are different to those in A.
>
> I.e. every element in B can either be in A, in L, or in neither but never
> in both.
>
> I have proved properties 1. and 2. in PVS. Now I need to prove
> the obvious property that if there is an element b in B
> such that b is not in A and not in L, then L contains less than N
> elements.
>
> A and L are modified in time-steps in which a number of elements can
> change their statuses but always ensuring that 1. and 2. hold.
>
> I have worked on this a long time and am reaching the desperate conclusion
> that it is not provable in PVS, requiring reasoning which cannot be
> expressed, such as the pigeon-hole principle.

The pigeonhole principle can certainly be expressed (and proven) in
PVS.  One form of the pigeonhole principle is in the finite_sets
library distributed with PVS2.3.  You should be able to use it (with a
little effort) to prove the property stated above.

--
-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/

```