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

[PVS-Help] Cotuple mutually exclusive component types



I have been working with cotuples.  I'm hitting a problem I don't know
how to solve.  The problem boils down to proving the following lemma:

cotuples: THEORY
 BEGIN

  new_type: TYPE = [nat + set[nat]]

  mutually_exclusive_types: LEMMA
    FORALL (obj: new_type): IN?_1(obj) /= IN?_2(obj)

 END cotuples


If I try (grind), it eliminates everything:


mutually_exclusive_types :  

  |-------
{1}   FORALL (obj: new_type): IN?_1(obj) /= IN?_2(obj)

Rule? (grind)
Trying repeated skolemization, instantiation, and if-lifting,
this simplifies to: 
mutually_exclusive_types :  

  |-------


Other rules give me both IN?_1(obj) and IN?_2(obj) on one side or the
other, but then I can't get anywhere with (smash), (assert), or any
other rule that seems likely to help.  How would one prove this?
-- 
Jerry James
http://www.ittc.ku.edu/~james/