Re: [PVS-Help] Unrecognized equality

[Jerome <jerome@xxxxxxxxxxxxxx>]

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
>