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

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
>