# Re: [PVS-Help] Unrecognized equality

```Here's another equality that should be straighforward, but PVS doesn't
seem to understand:

[-1]  t!1(e!1) o fold(t!1, U!1) = fold(t!1, U!1) o t!1(e!1)
[-2]  (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1))
[-3]  fold(s!1, U!1) o fold(t!1, U!1) =
fold(LAMBDA (k: D): s!1(k) o t!1(k), U!1)
|-------
[1]   U!1(e!1)
{2}   s!1(e!1) o fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1)) =
s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))

Rule? (replace -2 (2) :dir RL)
No change on: (REPLACE -2 (2) :DIR RL)
fold_distributive.2 :

[-1]  t!1(e!1) o fold(t!1, U!1) = fold(t!1, U!1) o t!1(e!1)
[-2]  (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1))
[-3]  fold(s!1, U!1) o fold(t!1, U!1) =
fold(LAMBDA (k: D): s!1(k) o t!1(k), U!1)
|-------
[1]   U!1(e!1)
{2}   s!1(e!1) o fold(s!1, U!1) o (fold(t!1, U!1) o t!1(e!1)) =
s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))

What I want is for [2] to become:

{2}   s!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1)) o t!1(e!1) =
s!1(e!1) o t!1(e!1) o (fold(s!1, U!1) o fold(t!1, U!1))

What could be going on? Unlike my last mysterious equality, doing a
check of 'show-expanded-sequent' doesn't yield any red flags...

jerome

On Tue, Jun 24, 2008 at 03:25:55PM -0700, Jerome 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
>

```