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.
•