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

[PVS-Help] Why I cannot replace here



Hello 

I don't know why I can't make a replace in the following sequent:

{-1}  (LAMBDA l: convergence(LAMBDA (n: nat): sigma(1 + j!1, n, a!1),
l)) =
       (LAMBDA l:
          convergence(LAMBDA (x: nat):
                        a!1(1 + j!1) + sigma(2 + j!1, x, a!1),
                      l))
[-2]  FORALL (F: [nat -> real], high, low: nat):
        high > low IMPLIES
         sigma(low, high, F) = F(low) + sigma(1 + low, high, F)
  |-------
[1]   epsilon(LAMBDA l:
                convergence(LAMBDA (n: nat): sigma(1 + j!1, n, a!1), l))
       =
       epsilon(LAMBDA l:
                 convergence(LAMBDA (x: nat):
                               a!1(1 + j!1) + sigma(2 + j!1, x, a!1),
                             l))


The expanded sequent is the following

{-1}  (LAMBDA l:
         analysis@convergence_sequences.convergence
             (LAMBDA (n: nat): reals@sigma[nat].sigma(1 + j!1, n, a!1),
l))
       =
       (LAMBDA l:
          analysis@convergence_sequences.convergence
              (LAMBDA (x: nat):
                 a!1(1 + j!1) + reals@sigma[nat].sigma(2 + j!1, x, a!1),
               l))
{-2}  FORALL (F: [nat -> real], high, low: nat):
        high > low IMPLIES
         reals@sigma[nat].sigma(low, high, F) =
          F(low) + reals@sigma[nat].sigma(1 + low, high, F)
  |-------
{1}   epsilon(LAMBDA l:
                analysis@convergence_sequences.convergence
                    (LAMBDA (n: nat):
                       reals@sigma[nat].sigma(1 + j!1, n, a!1),
                     l))
       =
       epsilon(LAMBDA l:
                 analysis@convergence_sequences.convergence
                     (LAMBDA (x: nat):
                        a!1(1 + j!1) +
                         reals@sigma[nat].sigma(2 + j!1, x, a!1),
                      l))

Thanks

Francisco Chaves