# Re: [PVS-Help] Unrecognized equality

```Ah ha! There's the culprit:

{-1}  equalities[value].=
(libext@fold[value, o].fold(s!1, J!1),
libext@fold[value, o].fold(s!1, K!1) o
libext@fold[value, o].fold
(s!1,
sets[libext@fold[value, o].index].difference(J!1, K!1)))
{-2}  sets[libext@fold[value, o].index].strict_subset?(K!1, J!1)
|-------
{1}   equalities[value].=
(libext@fold[value, o].fold(s!1, J!1),
libext@fold[value, o].fold(s!1, K!1) o
libext@fold[value, o].fold
(s!1, sets[types[N, value].index].difference(J!1, K!1)))

Thanks,

jerome

On Tue, Jun 24, 2008 at 03:32:45PM -0700, Sam Owre wrote:
>Hi Jerome,
>
>This usually means that the theory instances don't actually match.  Try
>running 'C-u M-x show-expanded-sequent' and see if that shows a
>difference.
>
>Regards,
>Sam
>
>
>Jerome <jerome@xxxxxxxxxxxxxx> wrote:
>
>> Does anyone know why the following doesn't produce Q.E.D in PVS?
>>
>>   {-1}  strict_subset?(K!1, J!1) IMPLIES
>> 	  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>   [-2]  strict_subset?(K!1, J!1)
>>     |-------
>>   [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>
>>   Rerunning step: (ASSERT)
>>   Simplifying, rewriting, and recording with decision procedures,
>>   this simplifies to:
>>   composable :
>>
>>   {-1}  fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>   [-2]  strict_subset?(K!1, J!1)
>>     |-------
>>   [1]   fold(s!1, J!1) = fold(s!1, K!1) o fold(s!1, difference(J!1, K!1))
>>
>> After I make ASSERT call I would think the proof was finished... am I
>> missing something? Thanks
>>
>> jerome
>

```