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

*To*: pvs-help@csl.sri.com*Subject*: A property I cannot prove in PVS*From*: Tamarah Arons <tamarah@wisdom.weizmann.ac.il>*Date*: Mon, 15 Nov 1999 12:32:12 +0200 (IST)*Delivery-Date*: Mon Nov 15 02:32:30 1999

Hello, 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. I realise that this is not the type of problems normally asked at pvs-help, but would really appreciate any ideas. Thanks, Tamarah

- Prev by Date:
**re: a question about a missing TCC** - Next by Date:
**Question on new decision procedures** - Prev by thread:
**Re: Question on new decision procedures** - Next by thread:
**Re: A property I cannot prove in PVS** - Index(es):