[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
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.