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

*To*: pvs-help@csl.sri.com*Subject*: reasoning with typepreds*From*: Mark Aronszajn <aronsz@csee.wvu.edu>*Date*: Thu, 30 Mar 2000 12:43:38 -0500 (EST)*Delivery-Date*: Thu Mar 30 09:46:07 2000

A TCC is generated by a theory I typechecked and in discharging that TCC I am faced with proving the following sequent: [-1] Sample_pred(s!1) |------- [1] s!1`Entry_Count(x1!1) >= 0 where variable 's!1' is of type Sample, and the antecedent was introduced by a call to (typepred "s!1"). The theory in question has a parameter for a type, Entry, and the type, Sample, is itself declared in the theory as follows: Sample: TYPE FROM [# Entry_Count: ({f: [Entry -> nat]| is_finite({y: Entry| f(y) > 0})}) Accepting: bool #] So I should be able to prove the above sequent if I can make use of the information in this type declaration. But what rule can I use to get at this information. I've come up against similar problems involving reasoning with the results of the typepred rule on several occasions. Can anyone help? Thanks in advance, Mark Aronszajn Reusable Software Research Group Dept. of Comp. Sci. & Elec. Eng. West Virginia University

- Prev by Date:
**Re: Don't understand this TCC** - Next by Date:
**cancelling typecheck-prove proof attempts** - Prev by thread:
**cancelling typecheck-prove proof attempts** - Next by thread:
**Don't understand this TCC** - Index(es):