# [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

```