Theorem: |
integral_mult |
not (?a contains ?bdv) => Integral ?a * ?b D ?bdv = ?a * Integral ?b D ?bdv |
instantiated by: | [(bdv, x)] |
to: | not (?b contains x) => Integral ?a * ?b D x = ?a * Integral ?b D x |
applied to: | Integral 1 D x + Integral 2*x D x + Integral x^2 D x |
at: | Integral 1 D x + Integral ?a * ?b D x + Integral x^2 D x |
under order: | dummy_order |
not (2 contains x) | ..evaluates
to.. |
True |
((could be
0..n assumptions)) |
..evaluates to.. | ((could be 0..n assumptions)) |
Integral ?a * ?b D x |
..matches..
|
Integral 2 * x D x |
?a
* Integral ?b D x |
..instantiates
to..
|
2 * Integral x D x |
results in: | Integral 1 D x + 2 * Integral x D x + Integral x^2 D x |
assuming: |
no assumption stored in the case
of evaluation to True or False |
evaluated by: |
eval_rls |
Explanations:
The precondition not (?b contains ?bdv) inhibits wrong applications of the rule as for instance
Integral x* x D x = Integral x D x * Integral x D x ((1))
This is wrong as you easily can verify: integrating the left hand side in (1) gives
Integral x* x D x = Integral x^2 D x = x^3/3 + c ((2))
while integrating the right hand sidein (1) gives
Integral x D x * Integral x D x = x^2/2 * x^2/2 + c = x^4/4 + c ((3))
Thus integrating the both sides in (1) gives two different
results (2) and (3) which should not happen (as long as we
want to perserve the meaning of '=' and the Integral to be
welldefined).