Computer Algebra and Symbolic Computation: Elementary Algorithms

In this section we state and prove a number of mathematical properties of the Free_of operator and use these properties to investigate the independence of generalized variables.
Theorem 6.33. Let u, v, and w be mathematical expressions.
If u ?v, then (Free_of(u,v) or Free_of(v, u)) ? true.
(Transitive Property) If Free_of(u, v) ? false and Free_of(v, w) ? false, then Free_of(u, w) ? false.
Proof: Both statements are easily proved. To show (1), if Free_of(u, v) and Free_of(v, u) are both false, then v is a complete sub-expression of u, and u is a complete sub-expression of v. The only way this can happen is for u= v. However, u ?v, and so either Free_of(u, v) or Free_of(v, u) must be true. (Of course, both can be true.)
To show (2), the hypothesis states that v is a complete sub-expression of u, and w is a complete sub-expression of v. Therefore, w is a complete sub-expression of u and Free_of(u, w) ? false.
The next theorem extends Theorem 6.33(1) to a set S of expressions.
Theorem 6.34. Let S={ x 1, x 2, , x m} be a set of mathematical expres sions ( with m ?2). Then, there is an...