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

*To*: PVS Help <pvs-help@xxxxxxxxxxx>*Subject*: [PVS-Help] Assumption inheritance*From*: Jerome White <jerome@xxxxxxxxxxxxxx>*Date*: Fri, 11 Sep 2009 11:50:00 -0700*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: Mutt/1.5.9i

Consider the following: A[T: TYPE, o: [T, T -> T]]: THEORY BEGIN ASSUMING commutative: ASSUMPTION commutative?(o) ENDASSUMING END A B[T: TYPE, o: [T, T -> T]]: THEORY BEGIN IMPORTING A[T, o] END B C[T: TYPE, o: [T, T -> T]]: THEORY BEGIN IMPORTING B[T, o] END C This hierarchy is a simplifed case of my theory collection. B has TCCS to prove based on the assumptions from A, while C has no TCCS. In my case, B does not have enough information to discharge its TCCS, but C does. Unfortunately, however, those TCCS aren't pushed down to C---is there a way to change this? Ideally, I would like the assuming-TCCS to show up all the way down the import chain until they are discharged. jerome

- Prev by Date:
**[PVS-HELP] Function type extend problem** - Next by Date:
**[PVS-Help] help - for modelling arrays** - Prev by thread:
**Re: [PVS-Help] help - for modelling arrays** - Next by thread:
**[PVS-HELP] Function type extend problem** - Index(es):