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

A property I cannot prove in PVS


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

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. 

I realise that this is not the type of problems normally asked at
pvs-help, but would really appreciate any ideas.