[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Assumption inheritance
Consider the following:
A[T: TYPE, o: [T, T -> T]]: THEORY BEGIN
commutative: ASSUMPTION commutative?(o)
B[T: TYPE, o: [T, T -> T]]: THEORY BEGIN
IMPORTING A[T, o]
C[T: TYPE, o: [T, T -> T]]: THEORY BEGIN
IMPORTING B[T, o]
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.