**A Proof Generated by Theorema**
Prove:
under the assumptions:
We assume
and show
Formula (1.1), by (Definition (limit:)), implies:
By (3), we can take an appropriate Skolem function such that
Formula (1.2), by (Definition (limit:)), implies:
By (5), we can take an appropriate Skolem function such that
Formula (2), using (Definition (limit:)), is implied by:
We assume
and show
We have to find such that
Formula (10), using (Definition (+:)), is implied by:
Formula (11), using (Lemma(|+|)), is implied by:
We have to find , and such that
Formula (13), using (6), is implied by:
which, using (4), is implied by:
which, using (Lemma (max)), is implied by:
Formula (14) is implied by:
Partially solving it, formula (15) is implied by:
Now,
can be solved for and by a call to Collins' CAD method yielding the solution
Let us take
Formula (16) is solved. Hence, we are done.
Copyright © 2001 Wolfram Media, Inc. All rights reserved.[Article Index][Prev Page][Next Page] |