Prove:

(Proposition (limit of sum)) ,

under the assumptions:

(Definition (limit:)) ,

(Definition (+:)) ,

(Lemma (|+|)) ,

(Lemma (max)) .

We assume

(1) ,

and show

(2) .

Formula (), by (), implies:

(3) .

By (), we can take an appropriate Skolem function such that

(4) ,

Formula (), by (), implies:

(5) .

By (), we can take an appropriate Skolem function such that

(6) ,

Formula (), using (), is implied by:

(7) .

We assume

(8) ,

and show

(9) .

We have to find   such that

(10) .

Formula (), using (), is implied by:

(11) .

Formula (), using (), is implied by:

(12) .

We have to find  , , and such that

(13) .

Formula (), using (), is implied by:

,

which, using (), is implied by:

,

which, using (), is implied by:

(14) .

Formula () is implied by

(15) .

Partially solving it, formula () is implied by

(16) .

Now,

can be solved for and by a call to Collins cad--method yielding a sample solution

,

.

Furthermore, we can immediately solve

for by taking

.

Hence formula () is solved, and we are done.

•

Additional Proof Generation Information

---

Converted by Mathematica      June 17, 2002