Re: [PVS-Help] Unrecognized equality

[Sam Owre <owre@xxxxxxxxxxx>]

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