[PVS-Help] Assumption inheritance

[Jerome White <jerome@xxxxxxxxxxxxxx>]

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