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
>